RellichKondrachov.Geometry.Manifold.Riemannian.VolumeMeasure

Define a canonical “volume” measure on a smooth Riemannian manifold as the Hausdorff measure at the manifold dimension, and record a finiteness-on-compacts / compact-manifold finiteness goal.

At the current Mathlib pin, a differential-form based construction of the Riemannian volume form is not available. The Hausdorff-measure route provides a fully-defined measure compatible with Riemannian isometries and suitable for building L²(M) once finiteness properties are in place.

Main definitions

• RellichKondrachov.Geometry.Manifold.Riemannian.riemannianVolumeMeasure: Hausdorff measure μH[dim] on M, using the emetric structure induced by the Riemannian metric.

@[implicit_reducible]

def RellichKondrachov.Geometry.Manifold.Riemannian.instMeasurableSpaceVolumeMeasure {M : Type u_3} [TopologicalSpace M] : MeasurableSpace M

Borel σ-algebra on the model space E.

Equations

• RellichKondrachov.Geometry.Manifold.Riemannian.instMeasurableSpaceVolumeMeasure = borel M

theorem RellichKondrachov.Geometry.Manifold.Riemannian.instBorelSpaceVolumeMeasure {M : Type u_3} [TopologicalSpace M] : BorelSpace M

noncomputable def RellichKondrachov.Geometry.Manifold.Riemannian.riemannianVolumeMeasure {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContinuousRiemannianBundle E fun (x : M) => TangentSpace I x] [T3Space M] : MeasureTheory.Measure M

The “Riemannian volume measure” as Hausdorff measure at the manifold dimension.

This uses EMetricSpace.ofRiemannianMetric to construct the emetric structure in a way that is defeq to the existing topology on M, as recommended by the Mathlib Riemannian manifold API.

Equations

• RellichKondrachov.Geometry.Manifold.Riemannian.riemannianVolumeMeasure I = MeasureTheory.Measure.hausdorffMeasure ↑(Module.finrank ℝ E)