RellichKondrachov.Geometry.Manifold.Sobolev.LocalizationH2

Chart-based localization of scalar functions on a compact manifold, at C² regularity.

This extends RellichKondrachov.Geometry.Manifold.Sobolev.Localization by showing that if f : M → ℝ is C² in the manifold sense, then its chart localization belongs to Euclidean C²_c (hence can be fed into the Euclidean H² baseline graph construction).

Main result

• RellichKondrachov.Geometry.Manifold.Sobolev.FiniteChartData.localize_mem_C2c

@[implicit_reducible]

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

Borel σ-algebra on the model space E.

Equations

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

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

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

For a C² function on a compact manifold, the chart-localization is a Euclidean C2c function.