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
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).
@[implicit_reducible]
def
RellichKondrachov.Geometry.Manifold.Sobolev.instMeasurableSpaceLocalization
{M : Type u_3}
[TopologicalSpace M]
:
Borel σ-algebra on the model space E.
Instances For
theorem
RellichKondrachov.Geometry.Manifold.Sobolev.instBorelSpaceLocalization
{M : Type u_3}
[TopologicalSpace M]
:
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
- One or more equations did not get rendered due to their size.
Instances For
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))
Instances For
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.ι)
:
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
Instances For
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.ι)
:
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.ι)
:
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.ι)
:
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.ι)
:
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 RellichKondrachov.Geometry.Manifold.Sobolev.Iℝ✝ 1 f)
(i : d.ι)
:
For a C^1 function on a compact manifold, the chart-localization is a Euclidean C1c
function.