RellichKondrachov.Geometry.Manifold.Sobolev.RellichKondrachovRiemannian.Chartwise

Chartwise compactness discharge for the manifold Rellich–Kondrachov theorem on compact Riemannian manifolds.

This module sets up the L²-range codomain restrictions and applies Euclidean Rellich compactness (on Lebesgue volume) after transporting along the L² equivalences from RellichKondrachovRiemannian.Transport.

@[implicit_reducible]

def RellichKondrachov.Geometry.Manifold.Sobolev.instMeasurableSpaceMChartwise {M : Type u_3} [TopologicalSpace M] : MeasurableSpace M

Borel σ-algebra on the manifold M.

Equations

• RellichKondrachov.Geometry.Manifold.Sobolev.instMeasurableSpaceMChartwise = borel M

theorem RellichKondrachov.Geometry.Manifold.Sobolev.instBorelSpaceMChartwise {M : Type u_3} [TopologicalSpace M] : BorelSpace M

@[implicit_reducible]

def RellichKondrachov.Geometry.Manifold.Sobolev.instMeasurableSpaceEChartwise {E : Type u_1} [NormedAddCommGroup E] : MeasurableSpace E

Borel σ-algebra on the model space E.

Equations

• RellichKondrachov.Geometry.Manifold.Sobolev.instMeasurableSpaceEChartwise = borel E

theorem RellichKondrachov.Geometry.Manifold.Sobolev.instBorelSpaceEChartwise {E : Type u_1} [NormedAddCommGroup E] : BorelSpace E

theorem RellichKondrachov.Geometry.Manifold.Sobolev.instOpensMeasurableSpaceChartwise {E : Type u_1} [NormedAddCommGroup E] : OpensMeasurableSpace E

theorem RellichKondrachov.Geometry.Manifold.Sobolev.instIsFiniteMeasureriemannianVolumeMeasureChartwise {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] (I : ModelWithCorners ℝ E H) [IsManifold I 1 M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContinuousRiemannianBundle E fun (x : M) => TangentSpace I x] [T3Space M] [CompactSpace M] : MeasureTheory.IsFiniteMeasure (Riemannian.riemannianVolumeMeasure I)

Chartwise compactness discharge (Riemannian volume)

This section uses Euclidean Rellich compactness on Lebesgue volume and transports it to the chart pushforward measures via the L² range equivalences developed above.

Range-codomain restricted chart maps

We will work with codomain restrictions into the closed extendByZero range to make the transport between μchart and volume explicit and purely L²-level.

noncomputable def RellichKondrachov.Geometry.Manifold.Sobolev.RiemannianFiniteChartData.h1ToChartL2Range {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] (I : ModelWithCorners ℝ E H) [IsManifold I ⊤ M] [IsManifold I 1 M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContinuousRiemannianBundle E fun (x : M) => TangentSpace I x] [I.Boundaryless] [T3Space M] [CompactSpace M] (dR : RiemannianFiniteChartData I) (i : dR.d.ι) : let μM := Riemannian.riemannianVolumeMeasure I; have μchart := dR.d.chartMeasure μM i; let K := dR.d.rhoSupportImage i; ↥(dR.d.h1 μM) →L[ℝ] ↥(MeasureTheory.Lp.extendByZeroₗᵢ ⋯).range

The chartwise H¹ → L² projection with codomain restricted to the Euclidean H¹ range, for the chart pushforward of the Riemannian volume measure.

Equations

• One or more equations did not get rendered due to their size.

Volume-side supported H¹ map and compactness

We now transport the chartwise H¹ element to Lebesgue volume on K, apply Euclidean Rellich compactness there, and transport the compactness statement back to the chart measure.

noncomputable def RellichKondrachov.Geometry.Manifold.Sobolev.RiemannianFiniteChartData.h1ToChartL2RangeVol {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] (I : ModelWithCorners ℝ E H) [IsManifold I ⊤ M] [IsManifold I 1 M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContinuousRiemannianBundle E fun (x : M) => TangentSpace I x] [I.Boundaryless] [T3Space M] [CompactSpace M] (dR : RiemannianFiniteChartData I) (i : dR.d.ι) : let μM := Riemannian.riemannianVolumeMeasure I; have _μchart := dR.d.chartMeasure μM i; let K := dR.d.rhoSupportImage i; ↥(dR.d.h1 μM) →L[ℝ] ↥(MeasureTheory.Lp.extendByZeroₗᵢ ⋯).range

The chartwise H¹ → L² projection into the Euclidean H¹ range, transported to Lebesgue volume on the fixed compact support.

Equations

• One or more equations did not get rendered due to their size.

A volume-side chart target map defined on the ambient H¹ target

For the closure argument showing membership in Euclidean H¹(volume), it is convenient to have a continuous linear map defined on the ambient chart H¹ target L²(μchart) × L²(μchart;E), rather than only on the extendByZero range.

We implement this by restricting to K, applying the restricted L² change-of-measure equivalence, and extending by zero back to L²(volume).

Graph compatibility (C¹c generators)

To use Euclidean Rellich compactness for volume, we need to know that the volume-side map chartTargetToVolumeTarget respects the Euclidean graph generators induced by FiniteChartData.localize.

Closure argument: chartwise volume image lies in Euclidean H¹(volume) and h1On

We use the graph compatibility lemma above to show that the volume-side projection map sends the defining dense range of FiniteChartData.h1 into the Euclidean graph range on volume, and thus extends to a map H¹(M) → H¹(volume) (and further into h1On K).

This sets up the application of Euclidean Rellich compactness on volume in later steps.

Compactness: chartwise H¹ → L² contribution

We now apply Euclidean Rellich compactness on Lebesgue volume (supported in K) and transport compactness back to the chart measure using the extendByZero-range equivalence.

theorem RellichKondrachov.Geometry.Manifold.Sobolev.RiemannianFiniteChartData.isCompactOperator_h1ToChartL2Range {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] (I : ModelWithCorners ℝ E H) [IsManifold I ⊤ M] [IsManifold I 1 M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContinuousRiemannianBundle E fun (x : M) => TangentSpace I x] [I.Boundaryless] [T3Space M] [CompactSpace M] (dR : RiemannianFiniteChartData I) (i : dR.d.ι) : have μM := Riemannian.riemannianVolumeMeasure I; IsCompactOperator ⇑(h1ToChartL2Range I dR i)