RellichKondrachov.Geometry.Manifold.Sobolev.H1

Define a scalar H¹ space on a compact manifold relative to finite chart data.

Given d : FiniteChartData and a finite measure μ on M, we:

• define the submodule C1 of C¹ scalar functions M → ℝ (in the manifold sense);
• define the per-chart graph map obtained by localizing into Euclidean C1c and then applying the Euclidean H¹ graph C1c →ₗ L² × L²(E);
• define h1 as the topological closure of the range of the product-of-charts graph map.

Main definitions

• RellichKondrachov.Geometry.Manifold.Sobolev.FiniteChartData.C1
• RellichKondrachov.Geometry.Manifold.Sobolev.FiniteChartData.h1

@[instance_reducible]

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

Borel σ-algebra on the model space E.

Equations

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

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

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

@[instance_reducible]

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

Borel σ-algebra on the manifold M.

Equations

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

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

def RellichKondrachov.Geometry.Manifold.Sobolev.FiniteChartData.C1 {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} : Submodule ℝ (M → ℝ)

C¹ scalar functions M → ℝ (in the manifold sense), as a submodule of M → ℝ.

Equations

• RellichKondrachov.Geometry.Manifold.Sobolev.FiniteChartData.C1 = { carrier := {f : M → ℝ | ContMDiff I (modelWithCornersSelf ℝ ℝ) 1 f}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

noncomputable def RellichKondrachov.Geometry.Manifold.Sobolev.FiniteChartData.localizeToC1c {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] [IsManifold I 1 M] [I.Boundaryless] [CompactSpace M] (d : FiniteChartData H M I) (i : d.ι) : ↥C1 →ₗ[ℝ] ↥Analysis.FunctionalSpaces.Sobolev.Euclidean.C1c

Localize a continuously differentiable manifold function to a compactly supported chart function.

Equations

• d.localizeToC1c i = { toFun := fun (f : ↥RellichKondrachov.Geometry.Manifold.Sobolev.FiniteChartData.C1) => ⟨d.localize (↑f) i, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }

Target types

@[reducible, inline]

abbrev RellichKondrachov.Geometry.Manifold.Sobolev.FiniteChartData.h1TargetE {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) (μ : MeasureTheory.Measure M) (i : d.ι) : Type u_1

The chartwise target type L² × L²(E) used to define manifold H¹.

Equations

• d.h1TargetE μ i = (↥(MeasureTheory.Lp ℝ 2 (d.chartMeasure μ i)) × ↥(MeasureTheory.Lp E 2 (d.chartMeasure μ i)))

@[reducible, inline]

abbrev RellichKondrachov.Geometry.Manifold.Sobolev.FiniteChartData.h1Target {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) (μ : MeasureTheory.Measure M) : Type (max u_1 u_4)

The product-of-charts target type used to define manifold H¹.

Equations

• d.h1Target μ = ((i : d.ι) → d.h1TargetE μ i)

noncomputable def RellichKondrachov.Geometry.Manifold.Sobolev.FiniteChartData.h1GraphChart {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 μ] (i : d.ι) : ↥C1 →ₗ[ℝ] d.h1TargetE μ i

The per-chart graph map C¹(M) →ₗ (L² × L²(E)) obtained by localization to chart i and the Euclidean H¹ graph construction.

Equations

• d.h1GraphChart μ i = RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.graph (d.chartMeasure μ i) ∘ₗ d.localizeToC1c i

theorem RellichKondrachov.Geometry.Manifold.Sobolev.FiniteChartData.h1GraphChart_mem_range_euclidean_graph {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 μ] (i : d.ι) (f : ↥C1) : (d.h1GraphChart μ i) f ∈ (Analysis.FunctionalSpaces.Sobolev.Euclidean.graph (d.chartMeasure μ i)).range

Unfolding lemmas

These lemmas expose the chartwise L² and L²(E) components of h1GraphChart in terms of the underlying localized function localize (d := d) f i. They are used downstream to control supports.

theorem RellichKondrachov.Geometry.Manifold.Sobolev.FiniteChartData.h1GraphChart_fst {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 μ] (i : d.ι) (f : ↥C1) : ((d.h1GraphChart μ i) f).1 = Analysis.FunctionalSpaces.Sobolev.Euclidean.toL2 (d.chartMeasure μ i) ⟨d.localize (↑f) i, ⋯⟩

The scalar L² component of h1GraphChart is the L² class of localize f i.

theorem RellichKondrachov.Geometry.Manifold.Sobolev.FiniteChartData.h1GraphChart_snd {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 μ] (i : d.ι) (f : ↥C1) : ((d.h1GraphChart μ i) f).2 = Analysis.FunctionalSpaces.Sobolev.Euclidean.toL2Grad (d.chartMeasure μ i) ⟨d.localize (↑f) i, ⋯⟩

The gradient L²(E) component of h1GraphChart is the L²(E) class of grad (localize f i).

noncomputable def RellichKondrachov.Geometry.Manifold.Sobolev.FiniteChartData.h1Graph {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.h1Target μ

The product-of-charts graph map C¹(M) →ₗ ∀ i, (L² × L²(E)) used to define manifold H¹.

Equations

• d.h1Graph μ = LinearMap.pi fun (i : d.ι) => d.h1GraphChart μ i

noncomputable def RellichKondrachov.Geometry.Manifold.Sobolev.FiniteChartData.h1 {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 μ] : Submodule ℝ (d.h1Target μ)

The H¹ submodule defined by chart localizations and the Euclidean H¹ graph construction.

Equations

• d.h1 μ = (d.h1Graph μ).range.topologicalClosure

theorem RellichKondrachov.Geometry.Manifold.Sobolev.FiniteChartData.isClosed_h1 {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 μ] : IsClosed ↑(d.h1 μ)

instance RellichKondrachov.Geometry.Manifold.Sobolev.FiniteChartData.instCompleteSpaceh1 {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 μ] : CompleteSpace ↥(d.h1 μ)

H¹ is complete (a Hilbert space once the ambient L² spaces are).

noncomputable def RellichKondrachov.Geometry.Manifold.Sobolev.FiniteChartData.h1ToChart {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 μ] (i : d.ι) : ↥(d.h1 μ) →L[ℝ] d.h1TargetE μ i

The continuous projection H¹ → chartwise L² × L²(E) for a fixed chart index.

Equations

• d.h1ToChart μ i = ContinuousLinearMap.proj i ∘SL (d.h1 μ).subtypeL

noncomputable def RellichKondrachov.Geometry.Manifold.Sobolev.FiniteChartData.h1ToChartL2 {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 μ] (i : d.ι) : ↥(d.h1 μ) →L[ℝ] ↥(MeasureTheory.Lp ℝ 2 (d.chartMeasure μ i))

The continuous chartwise L² map extracted from H¹.

Equations

• d.h1ToChartL2 μ i = ContinuousLinearMap.fst ℝ ↥(MeasureTheory.Lp ℝ 2 (d.chartMeasure μ i)) ↥(MeasureTheory.Lp E 2 (d.chartMeasure μ i)) ∘SL d.h1ToChart μ i

noncomputable def RellichKondrachov.Geometry.Manifold.Sobolev.FiniteChartData.h1ToChartL2Grad {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 μ] (i : d.ι) : ↥(d.h1 μ) →L[ℝ] ↥(MeasureTheory.Lp E 2 (d.chartMeasure μ i))

The continuous chartwise gradient map H¹ → L²(E) extracted from H¹.

Equations

• d.h1ToChartL2Grad μ i = ContinuousLinearMap.snd ℝ ↥(MeasureTheory.Lp ℝ 2 (d.chartMeasure μ i)) ↥(MeasureTheory.Lp E 2 (d.chartMeasure μ i)) ∘SL d.h1ToChart μ i