RellichKondrachov.Geometry.Manifold.Sobolev.H2

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 a manifold H² space as the topological closure of the range of a chartwise graph map into

L²(E, μᵢ) × (L²(E, μᵢ;E) × L²(E, μᵢ; E →L E))

where μᵢ is the pushforward chart measure (chartMeasure) and the graph map is obtained by:

1. localizing a C² function f : M → ℝ to a chart (extend-by-zero outside the chart target);
2. viewing it as an element of Euclidean C²_c;
3. applying the Euclidean H² graph map.

Main definitions

• RellichKondrachov.Geometry.Manifold.Sobolev.FiniteChartData.C2
• RellichKondrachov.Geometry.Manifold.Sobolev.FiniteChartData.h2

@[instance_reducible]

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

Borel σ-algebra on the model space E.

Equations

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

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

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

@[instance_reducible]

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

Borel σ-algebra on the manifold M.

Equations

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

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

def RellichKondrachov.Geometry.Manifold.Sobolev.FiniteChartData.C2 {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.C2 = { carrier := {f : M → ℝ | ContMDiff I (modelWithCornersSelf ℝ ℝ) 2 f}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

Target types

@[reducible, inline]

abbrev RellichKondrachov.Geometry.Manifold.Sobolev.FiniteChartData.h2TargetE {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) × L²(E →L E)) used to define manifold H².

Equations

• d.h2TargetE μ i = (↥(MeasureTheory.Lp ℝ 2 (d.chartMeasure μ i)) × ↥(MeasureTheory.Lp E 2 (d.chartMeasure μ i)) × ↥(MeasureTheory.Lp (E →L[ℝ] E) 2 (d.chartMeasure μ i)))

@[reducible, inline]

abbrev RellichKondrachov.Geometry.Manifold.Sobolev.FiniteChartData.h2Target {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.h2Target μ = ((i : d.ι) → d.h2TargetE μ i)

@[reducible, inline]

noncomputable abbrev RellichKondrachov.Geometry.Manifold.Sobolev.FiniteChartData.chartMeasureE {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.ι) : MeasureTheory.Measure E

The chart measure viewed on the model vector space.

Equations

• d.chartMeasureE μ i = d.chartMeasure μ i

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

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

Equations

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

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

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

Equations

• d.h2GraphChart μ i = RellichKondrachov.Analysis.FunctionalSpaces.Sobolev.Euclidean.graph2 (d.chartMeasureE μ i) ∘ₗ d.localizeToC2c i

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

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

Equations

• d.h2Graph μ = LinearMap.pi fun (i : d.ι) => d.h2GraphChart μ i

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

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

Equations

• d.h2 μ = (d.h2Graph μ).range.topologicalClosure

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

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

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

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

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

Equations

• d.h2ToChart μ i = ContinuousLinearMap.proj i ∘SL (d.h2 μ).subtypeL

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

The continuous chartwise L² map extracted from H².

Equations

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

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

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

Equations

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

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

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

Equations

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