Documentation

LeanPool.RellichKondrachov.Geometry.Manifold.Sobolev.ChartMeasureRiemannian

RellichKondrachov.Geometry.Manifold.Sobolev.ChartMeasureRiemannian #

Measure-comparison lemmas for chart pushforward measures arising from the Riemannian Hausdorff volume measure.

The key input is local Lipschitz control of chart inverses (in chart coordinates) for the Riemannian distance. This yields one-sided domination of chart measures by Euclidean Hausdorff measure on the chart target, restricted to suitable neighborhoods.

Main results #

source
@[implicit_reducible]
def RellichKondrachov.Geometry.Manifold.Sobolev.instMeasurableSpaceMChartMeasureRiemannian {M : Type uM} [TopologicalSpace M] :
MeasurableSpace M

Borel σ-algebra on the manifold M.

Equations
Instances For
    source
    theorem RellichKondrachov.Geometry.Manifold.Sobolev.instBorelSpaceMChartMeasureRiemannian {M : Type uM} [TopologicalSpace M] :
    BorelSpace M
    source
    @[implicit_reducible]
    def RellichKondrachov.Geometry.Manifold.Sobolev.instMeasurableSpaceEChartMeasureRiemannian {E : Type uE} [NormedAddCommGroup E] :
    MeasurableSpace E

    Borel σ-algebra on the model space E.

    Equations
    Instances For
      source
      theorem RellichKondrachov.Geometry.Manifold.Sobolev.instBorelSpaceEChartMeasureRiemannian {E : Type uE} [NormedAddCommGroup E] :
      BorelSpace E
      source
      theorem RellichKondrachov.Geometry.Manifold.Sobolev.instOpensMeasurableSpaceChartMeasureRiemannian {E : Type uE} [NormedAddCommGroup E] :
      OpensMeasurableSpace E
      source
      theorem RellichKondrachov.Geometry.Manifold.Sobolev.RiemannianFiniteChartData.chartMeasure_restrict_le_hausdorff {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] [IsManifold I 1 M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContinuousRiemannianBundle E fun (x : M) => TangentSpace I x] [T3Space M] (dR : RiemannianFiniteChartData I) (i : dR.d.ι) :
      (dR.d.chartMeasure (Riemannian.riemannianVolumeMeasure I) i).restrict (dR.chartBall i) ≤ ↑(dR.C i) ^ ↑(Module.finrank ℝ E) • (MeasureTheory.Measure.hausdorffMeasure ↑(Module.finrank ℝ E)).restrict (dR.chartBall i)

      On the chart ball, the chart pushforward measure of the Riemannian Hausdorff volume measure is dominated by Euclidean Hausdorff measure, with an explicit Lipschitz constant.

      Reverse domination on chart balls #

      source
      theorem RellichKondrachov.Geometry.Manifold.Sobolev.RiemannianFiniteChartData.hausdorff_restrict_le_chartMeasure {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] [IsManifold I 1 M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContinuousRiemannianBundle E fun (x : M) => TangentSpace I x] [T3Space M] (dR : RiemannianFiniteChartData I) (i : dR.d.ι) :
      (MeasureTheory.Measure.hausdorffMeasure ↑(Module.finrank ℝ E)).restrict (dR.chartBall i) ≤ ↑(dR.Cfwd i) ^ ↑(Module.finrank ℝ E) • (dR.d.chartMeasure (Riemannian.riemannianVolumeMeasure I) i).restrict (dR.chartBall i)

      On the chart ball, Euclidean Hausdorff measure is dominated by the chart pushforward measure of the Riemannian Hausdorff volume measure.