RellichKondrachov.Geometry.Manifold.Sobolev.ChartMeasureRiemannianVolume

Compare chart pushforward measures arising from the Riemannian Hausdorff volume measure against Lebesgue volume on the chart model space.

This is a convenience layer on top of RellichKondrachov.Geometry.Manifold.Sobolev.ChartMeasureRiemannian, which gives domination by the Euclidean Hausdorff measure μH[dim]. Since μH[finrank] is an additive Haar measure on finite-dimensional real inner product spaces, it is a scalar multiple of volume. We record the resulting domination by volume on chart balls.

Main results

• RellichKondrachov.Geometry.Manifold.Sobolev.RiemannianFiniteChartData. chartMeasure_restrict_le_volume
• RellichKondrachov.Geometry.Manifold.Sobolev.RiemannianFiniteChartData. volume_restrict_le_chartMeasure

@[implicit_reducible]

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

Borel σ-algebra on the manifold M.

Equations

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

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

@[implicit_reducible]

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

Borel σ-algebra on the model space E.

Equations

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

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

theorem RellichKondrachov.Geometry.Manifold.Sobolev.instOpensMeasurableSpaceEChartMeasureRiemannianVolume {E : Type uE} [NormedAddCommGroup E] : OpensMeasurableSpace E

Finiteness of comparison constants

The comparison lemmas in this file produce explicit ℝ≥0∞ constants. For downstream Lp change- of-measure equivalences we also need these constants to be finite (≠ ∞).

theorem RellichKondrachov.Geometry.Manifold.Sobolev.RiemannianFiniteChartData.chartMeasure_volume_constant_ne_top {E : Type uE} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ 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.ι) : ↑(dR.C i) ^ ↑(Module.finrank ℝ E) * ((MeasureTheory.Measure.hausdorffMeasure ↑(Module.finrank ℝ E)) (Metric.closedBall 0 1) / MeasureTheory.volume (Metric.closedBall 0 1)) ≠ ⊤

theorem RellichKondrachov.Geometry.Manifold.Sobolev.RiemannianFiniteChartData.volume_chartMeasure_constant_ne_top {E : Type uE} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ 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.ι) : MeasureTheory.volume (Metric.closedBall 0 1) / (MeasureTheory.Measure.hausdorffMeasure ↑(Module.finrank ℝ E)) (Metric.closedBall 0 1) * ↑(dR.Cfwd i) ^ ↑(Module.finrank ℝ E) ≠ ⊤

theorem RellichKondrachov.Geometry.Manifold.Sobolev.RiemannianFiniteChartData.chartMeasure_restrict_le_volume {E : Type uE} [NormedAddCommGroup E] [InnerProductSpace ℝ 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] [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)) (Metric.closedBall 0 1) / MeasureTheory.volume (Metric.closedBall 0 1))) • MeasureTheory.volume.restrict (dR.chartBall i)

On the chart ball, the chart pushforward measure of the Riemannian Hausdorff volume measure is dominated by Lebesgue volume on the chart model space.

theorem RellichKondrachov.Geometry.Manifold.Sobolev.RiemannianFiniteChartData.volume_restrict_le_chartMeasure {E : Type uE} [NormedAddCommGroup E] [InnerProductSpace ℝ 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] [T3Space M] (dR : RiemannianFiniteChartData I) (i : dR.d.ι) : MeasureTheory.volume.restrict (dR.chartBall i) ≤ (MeasureTheory.volume (Metric.closedBall 0 1) / (MeasureTheory.Measure.hausdorffMeasure ↑(Module.finrank ℝ E)) (Metric.closedBall 0 1) * ↑(dR.Cfwd i) ^ ↑(Module.finrank ℝ E)) • (dR.d.chartMeasure (Riemannian.riemannianVolumeMeasure I) i).restrict (dR.chartBall i)

On the chart ball, Lebesgue volume on the chart model space is dominated by the chart pushforward measure of the Riemannian Hausdorff volume measure.