RellichKondrachov.Geometry.Manifold.Sobolev.Localization

Chart-based localization of scalar functions on a compact manifold.

Given finite chart data d : FiniteChartData (a finite family of chart centers with a smooth partition of unity subordinate to those charts), we define a localization operation

localize d f i : E → ℝ

on the model space E, obtained by pulling back ρ_i • f along the extended chart (extChartAt I (d.center i)).symm and extending by 0 outside the chart target.

For compact manifolds, the resulting function has compact support and is C^1 (hence belongs to the Euclidean C1c submodule used in the Euclidean Sobolev baseline).

@[instance_reducible]

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

Borel σ-algebra on the model space E.

Equations

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

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

@[reducible, inline]

noncomputable abbrev RellichKondrachov.Geometry.Manifold.Sobolev.Iℝ : ModelWithCorners ℝ ℝ ℝ

The standard model with corners on the real line.

Equations

• RellichKondrachov.Geometry.Manifold.Sobolev.Iℝ = modelWithCornersSelf ℝ ℝ

@[reducible, inline]

noncomputable abbrev RellichKondrachov.Geometry.Manifold.Sobolev.FiniteChartData.chart {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) (i : d.ι) : PartialEquiv M E

The extended chart centered at the selected point of the finite chart family.

Equations

• d.chart i = extChartAt I (d.center i)

noncomputable def RellichKondrachov.Geometry.Manifold.Sobolev.FiniteChartData.localize {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 : M → ℝ) (i : d.ι) : E → ℝ

The localization of a scalar function f : M → ℝ to a chart i, as a function on E.

Equations

• d.localize f i = (d.chart i).target.indicator fun (y : E) => (d.ρ i) (↑(d.chart i).symm y) * f (↑(d.chart i).symm y)

def RellichKondrachov.Geometry.Manifold.Sobolev.FiniteChartData.rhoSupportClosure {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) (i : d.ι) : Set M

The closed set closure (support (ρ i)) used to control the support of localizations.

Equations

• d.rhoSupportClosure i = closure (Function.support ⇑(d.ρ i))

theorem RellichKondrachov.Geometry.Manifold.Sobolev.FiniteChartData.rhoSupportClosure_subset_source {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) (i : d.ι) : d.rhoSupportClosure i ⊆ (d.chart i).source

theorem RellichKondrachov.Geometry.Manifold.Sobolev.FiniteChartData.isCompact_rhoSupportClosure {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] [CompactSpace M] (d : FiniteChartData H M I) (i : d.ι) : IsCompact (d.rhoSupportClosure i)

def RellichKondrachov.Geometry.Manifold.Sobolev.FiniteChartData.rhoSupportImage {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) (i : d.ι) : Set E

A compact subset of the chart model space containing the supports of all localizations.

Equations

• d.rhoSupportImage i = ↑(d.chart i) '' d.rhoSupportClosure i

theorem RellichKondrachov.Geometry.Manifold.Sobolev.FiniteChartData.isCompact_rhoSupportImage {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] [CompactSpace M] (d : FiniteChartData H M I) (i : d.ι) : IsCompact (d.rhoSupportImage i)

theorem RellichKondrachov.Geometry.Manifold.Sobolev.FiniteChartData.support_localize_subset_rhoSupportImage {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 : M → ℝ) (i : d.ι) : Function.support (d.localize f i) ⊆ d.rhoSupportImage i

theorem RellichKondrachov.Geometry.Manifold.Sobolev.FiniteChartData.tsupport_localize_subset_rhoSupportImage {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] [CompactSpace M] (d : FiniteChartData H M I) (f : M → ℝ) (i : d.ι) : tsupport (d.localize f i) ⊆ d.rhoSupportImage i

theorem RellichKondrachov.Geometry.Manifold.Sobolev.FiniteChartData.rhoSupportImage_subset_target {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) (i : d.ι) : d.rhoSupportImage i ⊆ (d.chart i).target

theorem RellichKondrachov.Geometry.Manifold.Sobolev.FiniteChartData.tsupport_localize_subset_target {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] [CompactSpace M] (d : FiniteChartData H M I) (f : M → ℝ) (i : d.ι) : tsupport (d.localize f i) ⊆ (d.chart i).target

theorem RellichKondrachov.Geometry.Manifold.Sobolev.FiniteChartData.hasCompactSupport_localize {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] [CompactSpace M] (d : FiniteChartData H M I) (f : M → ℝ) (i : d.ι) : HasCompactSupport (d.localize f i)

theorem RellichKondrachov.Geometry.Manifold.Sobolev.FiniteChartData.localize_mem_C1c {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) {f : M → ℝ} (hf : ContMDiff I Iℝ 1 f) (i : d.ι) : d.localize f i ∈ Analysis.FunctionalSpaces.Sobolev.Euclidean.C1c

For a C^1 function on a compact manifold, the chart-localization is a Euclidean C1c function.