RellichKondrachov.Geometry.Manifold.Sobolev.ChartDataRiemannian

Riemannian-specialized chart/partition-of-unity data for Sobolev theory.

This file constructs finite chart data on a compact Riemannian manifold, with the additional guarantee that each partition-of-unity function is supported in a chart neighborhood on which the inverse extended chart is Lipschitz (with respect to the Riemannian distance).

This is the natural input needed to compare chart pushforward measures against Euclidean Hausdorff measure on the fixed compact supports used by the manifold Rellich glue.

Main definitions / results

• RellichKondrachov.Geometry.Manifold.Sobolev.RiemannianFiniteChartData
• RellichKondrachov.Geometry.Manifold.Sobolev.exists_riemannianFiniteChartData

@[implicit_reducible]

def RellichKondrachov.Geometry.Manifold.Sobolev.instMeasurableSpaceMChartDataRiemannian {M : Type uM} [TopologicalSpace M] : MeasurableSpace M

Borel σ-algebra on the manifold M.

Equations

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

theorem RellichKondrachov.Geometry.Manifold.Sobolev.instBorelSpaceMChartDataRiemannian {M : Type uM} [TopologicalSpace M] : BorelSpace M

@[implicit_reducible]

def RellichKondrachov.Geometry.Manifold.Sobolev.instMeasurableSpaceEChartDataRiemannian {E : Type uE} [NormedAddCommGroup E] : MeasurableSpace E

Borel σ-algebra on the model space E.

Equations

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

theorem RellichKondrachov.Geometry.Manifold.Sobolev.instBorelSpaceEChartDataRiemannian {E : Type uE} [NormedAddCommGroup E] : BorelSpace E

structure RellichKondrachov.Geometry.Manifold.Sobolev.RiemannianFiniteChartData {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type uH} [TopologicalSpace H] {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] (I : ModelWithCorners ℝ E H) [IsManifold I ⊤ M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] : Type (uM + 1)

A FiniteChartData together with explicit Lipschitz neighborhoods (in chart coordinates) for the inverse extended chart, and a partition-of-unity subordination guarantee to those neighborhoods.

• d : FiniteChartData H M I

  Underlying finite chart data.

• C : self.d.ι → NNReal

  Lipschitz constant for each chart inverse on a fixed ball.

• Cfwd : self.d.ι → NNReal

  Lipschitz constant for each (forward) extended chart on the preimage of the chart ball.

• r : self.d.ι → ℝ

  Radius of the chart ball on which the inverse is Lipschitz.

• r_pos (i : self.d.ι) : 0 < self.r i

  Positivity of the radii.

• riemannianLipschitz_symm (i : self.d.ι) (y₁ : E) : y₁ ∈ Metric.ball (↑(extChartAt I (self.d.center i)) (self.d.center i)) (self.r i) ∩ Set.range ↑I → ∀ y₂ ∈ Metric.ball (↑(extChartAt I (self.d.center i)) (self.d.center i)) (self.r i) ∩ Set.range ↑I, Manifold.riemannianEDist I (↑(extChartAt I (self.d.center i)).symm y₁) (↑(extChartAt I (self.d.center i)).symm y₂) ≤ ↑(self.C i) * edist y₁ y₂

  Riemannian-distance Lipschitz control of the inverse extended chart on the chart ball.

• riemannianLipschitz (i : self.d.ι) (x₁ : M) : x₁ ∈ ↑(extChartAt I (self.d.center i)) ⁻¹' Metric.ball (↑(extChartAt I (self.d.center i)) (self.d.center i)) (self.r i) ∩ (extChartAt I (self.d.center i)).source → ∀ x₂ ∈ ↑(extChartAt I (self.d.center i)) ⁻¹' Metric.ball (↑(extChartAt I (self.d.center i)) (self.d.center i)) (self.r i) ∩ (extChartAt I (self.d.center i)).source, edist (↑(extChartAt I (self.d.center i)) x₁) (↑(extChartAt I (self.d.center i)) x₂) ≤ ↑(self.Cfwd i) * Manifold.riemannianEDist I x₁ x₂

  Riemannian-distance Lipschitz control of the (forward) extended chart on the preimage of the chart ball (inside the chart source).

• subordinate_ball (i : self.d.ι) : closure (Function.support ⇑(self.d.ρ i)) ⊆ ↑(extChartAt I (self.d.center i)) ⁻¹' Metric.ball (↑(extChartAt I (self.d.center i)) (self.d.center i)) (self.r i) ∩ (extChartAt I (self.d.center i)).source

  The partition-of-unity is subordinate to the preimage of the chart ball (inside the chart source).

Chart balls

The RiemannianFiniteChartData structure equips each chart index with a radius r i. The corresponding chart ball is the intersection of the Euclidean metric ball in chart coordinates with the chart target.

This set is used throughout the Sobolev/Rellich development to localize measure comparisons and compactness arguments.

def RellichKondrachov.Geometry.Manifold.Sobolev.RiemannianFiniteChartData.chartBall {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type uH} [TopologicalSpace H] {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] {I : ModelWithCorners ℝ E H} [IsManifold I ⊤ M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] (dR : RiemannianFiniteChartData I) (i : dR.d.ι) : Set E

The chart ball in model-space coordinates associated to chart index i.

Equations

• dR.chartBall i = Metric.ball (↑(extChartAt I (dR.d.center i)) (dR.d.center i)) (dR.r i) ∩ (extChartAt I (dR.d.center i)).target

theorem RellichKondrachov.Geometry.Manifold.Sobolev.exists_riemannianFiniteChartData {E : Type uE} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type uH} [TopologicalSpace H] {M : Type uM} [TopologicalSpace M] [ChartedSpace H M] (I : ModelWithCorners ℝ E H) [IsManifold I ⊤ M] [IsManifold I 1 M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContinuousRiemannianBundle E fun (x : M) => TangentSpace I x] [T2Space M] [CompactSpace M] : Nonempty (RiemannianFiniteChartData I)

On a compact Riemannian manifold, there exists finite chart data together with explicit Lipschitz neighborhoods (in chart coordinates) for chart inverses and a partition-of-unity subordination to those neighborhoods.