RellichKondrachov.Geometry.Manifold.Sobolev.EmbeddingL2

Define the canonical continuous linear maps H¹ → L² and H² → L² on a compact manifold, relative to finite chart data.

The construction is by summing, over the finite chart index type, the chartwise L² components (coming from h1ToChartL2 / h2ToChartL2) pulled back to M via a measure-preserving chart map and then extended by zero from the chart source.

Main definitions

• RellichKondrachov.Geometry.Manifold.Sobolev.FiniteChartData.chartToGlobalL2
• RellichKondrachov.Geometry.Manifold.Sobolev.FiniteChartData.h1ToL2
• RellichKondrachov.Geometry.Manifold.Sobolev.FiniteChartData.h2ToL2

@[implicit_reducible]

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

Borel σ-algebra on the manifold M.

Equations

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

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

@[implicit_reducible]

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

Borel σ-algebra on the model space E.

Equations

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

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

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

noncomputable def RellichKondrachov.Geometry.Manifold.Sobolev.FiniteChartData.chartToGlobalL2 {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] (d : FiniteChartData H M I) {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] (μ : MeasureTheory.Measure M) (i : d.ι) : ↥(MeasureTheory.Lp F 2 (d.chartMeasure μ i)) →L[ℝ] ↥(MeasureTheory.Lp F 2 μ)

The chartwise-to-global L² map on the manifold: pull back along a measure-preserving chart map and extend by zero from the chart source.

Equations

• d.chartToGlobalL2 μ i = (MeasureTheory.Lp.extendByZeroₗᵢ ⋯).toContinuousLinearMap ∘SL (d.chartPullbackL2 μ i).toContinuousLinearMap

noncomputable def RellichKondrachov.Geometry.Manifold.Sobolev.FiniteChartData.h1ToL2 {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace 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] [I.Boundaryless] [CompactSpace M] (d : FiniteChartData H M I) (μ : MeasureTheory.Measure M) [MeasureTheory.IsFiniteMeasure μ] : ↥(d.h1 μ) →L[ℝ] ↥(MeasureTheory.Lp ℝ 2 μ)

The continuous linear inclusion H¹(d,μ) → L²(M,μ) defined by summing the chartwise L² components after pulling them back to M and extending by zero.

Equations

• d.h1ToL2 μ = ∑ i : d.ι, d.chartToGlobalL2 μ i ∘SL d.h1ToChartL2 μ i

noncomputable def RellichKondrachov.Geometry.Manifold.Sobolev.FiniteChartData.h2ToL2 {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {H : Type u_2} [TopologicalSpace H] {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [IsManifold I ⊤ M] [I.Boundaryless] [CompactSpace M] (d : FiniteChartData H M I) (μ : MeasureTheory.Measure M) [MeasureTheory.IsFiniteMeasure μ] : ↥(d.h2 μ) →L[ℝ] ↥(MeasureTheory.Lp ℝ 2 μ)

The continuous linear inclusion H²(d,μ) → L²(M,μ) defined by summing the chartwise L² components after pulling them back to M and extending by zero.

Equations

• d.h2ToL2 μ = ∑ i : d.ι, d.chartToGlobalL2 μ i ∘SL d.h2ToChartL2 μ i

noncomputable def RellichKondrachov.Geometry.Manifold.Sobolev.FiniteChartData.c1ToH1 {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace 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] [I.Boundaryless] [CompactSpace M] (d : FiniteChartData H M I) (μ : MeasureTheory.Measure M) [MeasureTheory.IsFiniteMeasure μ] : ↥C1 →ₗ[ℝ] ↥(d.h1 μ)

The canonical linear map C¹(M) →ₗ H¹(d,μ) landing in the dense range used to define H¹.

Equations

• d.c1ToH1 μ = LinearMap.codRestrict (d.h1 μ) (d.h1Graph μ) ⋯

noncomputable def RellichKondrachov.Geometry.Manifold.Sobolev.FiniteChartData.c1ToL2 {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace 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] [I.Boundaryless] [CompactSpace M] (d : FiniteChartData H M I) (μ : MeasureTheory.Measure M) [MeasureTheory.IsFiniteMeasure μ] : ↥C1 →ₗ[ℝ] ↥(MeasureTheory.Lp ℝ 2 μ)

The linear map C¹(M) →ₗ L²(M,μ) obtained by summing the per-chart L² localizations pulled back to M and extended by zero.

Equations

• d.c1ToL2 μ = ∑ i : d.ι, ↑(d.chartToGlobalL2 μ i) ∘ₗ LinearMap.fst ℝ ↥(MeasureTheory.Lp ℝ 2 (d.chartMeasure μ i)) ↥(MeasureTheory.Lp E 2 (d.chartMeasure μ i)) ∘ₗ d.h1GraphChart μ i

theorem RellichKondrachov.Geometry.Manifold.Sobolev.FiniteChartData.h1ToL2_c1ToH1 {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace 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] [I.Boundaryless] [CompactSpace M] (d : FiniteChartData H M I) (μ : MeasureTheory.Measure M) [MeasureTheory.IsFiniteMeasure μ] (f : ↥C1) : (d.h1ToL2 μ) ((d.c1ToH1 μ) f) = (d.c1ToL2 μ) f

noncomputable def RellichKondrachov.Geometry.Manifold.Sobolev.FiniteChartData.c2ToH2 {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {H : Type u_2} [TopologicalSpace H] {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [IsManifold I ⊤ M] [I.Boundaryless] [CompactSpace M] (d : FiniteChartData H M I) (μ : MeasureTheory.Measure M) [MeasureTheory.IsFiniteMeasure μ] : ↥C2 →ₗ[ℝ] ↥(d.h2 μ)

The canonical linear map C²(M) →ₗ H²(d,μ) landing in the dense range used to define H².

Equations

• d.c2ToH2 μ = LinearMap.codRestrict (d.h2 μ) (d.h2Graph μ) ⋯

noncomputable def RellichKondrachov.Geometry.Manifold.Sobolev.FiniteChartData.c2ToL2 {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {H : Type u_2} [TopologicalSpace H] {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [IsManifold I ⊤ M] [I.Boundaryless] [CompactSpace M] (d : FiniteChartData H M I) (μ : MeasureTheory.Measure M) [MeasureTheory.IsFiniteMeasure μ] : ↥C2 →ₗ[ℝ] ↥(MeasureTheory.Lp ℝ 2 μ)

The linear map C²(M) →ₗ L²(M,μ) obtained by summing the per-chart L² localizations pulled back to M and extended by zero.

Equations

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

theorem RellichKondrachov.Geometry.Manifold.Sobolev.FiniteChartData.h2ToL2_c2ToH2 {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [CompleteSpace E] {H : Type u_2} [TopologicalSpace H] {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [IsManifold I ⊤ M] [I.Boundaryless] [CompactSpace M] (d : FiniteChartData H M I) (μ : MeasureTheory.Measure M) [MeasureTheory.IsFiniteMeasure μ] (f : ↥C2) : (d.h2ToL2 μ) ((d.c2ToH2 μ) f) = (d.c2ToL2 μ) f