RellichKondrachov.Geometry.Manifold.Sobolev.RellichKondrachovRiemannian.Transport

Change-of-measure and extendByZero transport lemmas used in the Riemannian Rellich–Kondrachov compactness proof.

Main definitions

• l2EquivVolumeOnRhoSupportImage / l2ExtendByZeroRangeEquivVolumeOnRhoSupportImage: L²-level equivalences between the chart pushforward measure of the Riemannian volume and Lebesgue volume, localized to the fixed compact support FiniteChartData.rhoSupportImage.
• rhoSupportImage_measurable: measurability of the fixed support set.

@[implicit_reducible]

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

Borel σ-algebra on the manifold M.

Equations

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

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

@[implicit_reducible]

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

Borel σ-algebra on the model space E.

Equations

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

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

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

theorem RellichKondrachov.Geometry.Manifold.Sobolev.instIsFiniteMeasureriemannianVolumeMeasure {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)

Support control

We will use a fixed compact set in the chart model space containing the supports of all localized functions. In the Riemannian-specialized finite chart data, this set sits inside the chart ball.

theorem RellichKondrachov.Geometry.Manifold.Sobolev.RiemannianFiniteChartData.rhoSupportImage_subset_chartBall {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] (I : ModelWithCorners ℝ E H) [IsManifold I ⊤ M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] (dR : RiemannianFiniteChartData I) (i : dR.d.ι) : dR.d.rhoSupportImage i ⊆ dR.chartBall i

Measure comparison on the fixed compact support

Downstream L² change-of-measure equivalences require finite domination constants. The Riemannian chart-measure comparison lemmas provide explicit constants on the chart ball; the support-control lemma above lets us restrict those inequalities to the compact support set FiniteChartData.rhoSupportImage.

theorem RellichKondrachov.Geometry.Manifold.Sobolev.RiemannianFiniteChartData.rhoSupportImage_measurable {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {H : Type u_2} [TopologicalSpace H] {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [IsManifold I ⊤ M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [CompactSpace M] (dR : RiemannianFiniteChartData I) (i : dR.d.ι) : MeasurableSet (dR.d.rhoSupportImage i)

L² support for the chartwise H¹ projection

For each chart i, the scalar L² component of the manifold H¹ element is (a.e.) supported in rhoSupportImage i. We record this as membership in the range of extendByZeroₗᵢ from the restricted measure.

Chart coordinate lands in Euclidean H¹

The manifold H¹ is built from the Euclidean graph construction chartwise, hence each chart coordinate of a manifold H¹ element belongs to the corresponding Euclidean H¹ space.

Codomain restriction: chart coordinate as a Euclidean H¹ element

We package h1ToChart_mem_euclidean_h1 as a codomain-restricted continuous linear map landing in the Euclidean H¹ submodule.

Codomain restriction: chart coordinate in supported Euclidean H¹

Using the L² support lemma (h1ToChartL2_mem_extendByZero_range), we further restrict the chartwise Euclidean H¹ element to the supported subspace h1OnMeasure μchart (rhoSupportImage i).

theorem RellichKondrachov.Geometry.Manifold.Sobolev.RiemannianFiniteChartData.h1ToChartL2_mem_extendByZero_range {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.ι) (x : ↥(dR.d.h1 (Riemannian.riemannianVolumeMeasure I))) : let μM := Riemannian.riemannianVolumeMeasure I; let μchart := dR.d.chartMeasure μM i; let K := dR.d.rhoSupportImage i; (dR.d.h1ToChartL2 μM i) x ∈ (MeasureTheory.Lp.extendByZeroₗᵢ ⋯).range

theorem RellichKondrachov.Geometry.Manifold.Sobolev.RiemannianFiniteChartData.h1ToChartL2Grad_mem_extendByZero_range {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.ι) (x : ↥(dR.d.h1 (Riemannian.riemannianVolumeMeasure I))) : let μM := Riemannian.riemannianVolumeMeasure I; let μchart := dR.d.chartMeasure μM i; let K := dR.d.rhoSupportImage i; (dR.d.h1ToChartL2Grad μM i) x ∈ (MeasureTheory.Lp.extendByZeroₗᵢ ⋯).range

theorem RellichKondrachov.Geometry.Manifold.Sobolev.RiemannianFiniteChartData.chartMeasure_restrict_rhoSupportImage_le_volume {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] [T3Space M] [CompactSpace M] (dR : RiemannianFiniteChartData I) (i : dR.d.ι) : have μM := Riemannian.riemannianVolumeMeasure I; have μchart := dR.d.chartMeasure μM i; μchart.restrict (dR.d.rhoSupportImage i) ≤ (↑(dR.C i) ^ ↑(Module.finrank ℝ E) * ((MeasureTheory.Measure.hausdorffMeasure ↑(Module.finrank ℝ E)) (Metric.closedBall 0 1) / MeasureTheory.volume (Metric.closedBall 0 1))) • MeasureTheory.volume.restrict (dR.d.rhoSupportImage i)

theorem RellichKondrachov.Geometry.Manifold.Sobolev.RiemannianFiniteChartData.volume_restrict_rhoSupportImage_le_chartMeasure {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] [T3Space M] [CompactSpace M] (dR : RiemannianFiniteChartData I) (i : dR.d.ι) : have μM := Riemannian.riemannianVolumeMeasure I; have μchart := dR.d.chartMeasure μM i; MeasureTheory.volume.restrict (dR.d.rhoSupportImage i) ≤ (MeasureTheory.volume (Metric.closedBall 0 1) / (MeasureTheory.Measure.hausdorffMeasure ↑(Module.finrank ℝ E)) (Metric.closedBall 0 1) * ↑(dR.Cfwd i) ^ ↑(Module.finrank ℝ E)) • μchart.restrict (dR.d.rhoSupportImage i)

L² equivalence on the compact support

On FiniteChartData.rhoSupportImage i, the chart pushforward measure of the Riemannian volume is mutually comparable with Lebesgue volume. This yields a continuous linear equivalence between the restricted L² spaces.

noncomputable def RellichKondrachov.Geometry.Manifold.Sobolev.RiemannianFiniteChartData.l2EquivVolumeOnRhoSupportImage' {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] [T3Space M] [CompactSpace M] (dR : RiemannianFiniteChartData I) (i : dR.d.ι) (F : Type u_4) [NormedAddCommGroup F] [NormedSpace ℝ F] : ↥(MeasureTheory.Lp F 2 ((dR.d.chartMeasure (Riemannian.riemannianVolumeMeasure I) i).restrict (dR.d.rhoSupportImage i))) ≃L[ℝ] ↥(MeasureTheory.Lp F 2 (MeasureTheory.volume.restrict (dR.d.rhoSupportImage i)))

The L²-level equivalence between the chart pushforward measure and Lebesgue volume, localized to the fixed compact support, for a general value type F.

Equations

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

noncomputable def RellichKondrachov.Geometry.Manifold.Sobolev.RiemannianFiniteChartData.l2EquivVolumeOnRhoSupportImage {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] [T3Space M] [CompactSpace M] (dR : RiemannianFiniteChartData I) (i : dR.d.ι) : ↥(MeasureTheory.Lp ℝ 2 ((dR.d.chartMeasure (Riemannian.riemannianVolumeMeasure I) i).restrict (dR.d.rhoSupportImage i))) ≃L[ℝ] ↥(MeasureTheory.Lp ℝ 2 (MeasureTheory.volume.restrict (dR.d.rhoSupportImage i)))

The scalar (ℝ-valued) L²-level equivalence between the chart pushforward measure and Lebesgue volume, localized to the fixed compact support.

Equations

• dR.l2EquivVolumeOnRhoSupportImage i = dR.l2EquivVolumeOnRhoSupportImage' i ℝ

Range equivalence for extendByZeroₗᵢ on the compact support

The range of extension-by-zero from μ.restrict K is canonically isomorphic to the restricted L² space. Combining this with l2EquivVolumeOnRhoSupportImage yields a (continuous) linear equivalence between the extendByZero ranges for μchart and Lebesgue volume.

noncomputable def RellichKondrachov.Geometry.Manifold.Sobolev.RiemannianFiniteChartData.l2ExtendByZeroRangeEquivVolumeOnRhoSupportImage' {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] [T3Space M] [CompactSpace M] (dR : RiemannianFiniteChartData I) (i : dR.d.ι) (F : Type u_4) [NormedAddCommGroup F] [NormedSpace ℝ F] : have μM := Riemannian.riemannianVolumeMeasure I; have μchart := dR.d.chartMeasure μM i; let K := dR.d.rhoSupportImage i; ↥(MeasureTheory.Lp.extendByZeroₗᵢ ⋯).range ≃L[ℝ] ↥(MeasureTheory.Lp.extendByZeroₗᵢ ⋯).range

The extension-by-zero range equivalence between the chart pushforward measure and Lebesgue volume on the fixed compact support, for a general value type F.

Equations

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

noncomputable def RellichKondrachov.Geometry.Manifold.Sobolev.RiemannianFiniteChartData.l2ExtendByZeroRangeEquivVolumeOnRhoSupportImage {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] [T3Space M] [CompactSpace M] (dR : RiemannianFiniteChartData I) (i : dR.d.ι) : have μM := Riemannian.riemannianVolumeMeasure I; have μchart := dR.d.chartMeasure μM i; let K := dR.d.rhoSupportImage i; ↥(MeasureTheory.Lp.extendByZeroₗᵢ ⋯).range ≃L[ℝ] ↥(MeasureTheory.Lp.extendByZeroₗᵢ ⋯).range

The scalar (ℝ-valued) extension-by-zero range equivalence between the chart pushforward measure and Lebesgue volume on the fixed compact support.

Equations

• dR.l2ExtendByZeroRangeEquivVolumeOnRhoSupportImage i = dR.l2ExtendByZeroRangeEquivVolumeOnRhoSupportImage' i ℝ