RellichKondrachov.Geometry.Manifold.Riemannian.VolumeMeasure.Finiteness

Finiteness properties of riemannianVolumeMeasure.

Main results

• RellichKondrachov.Geometry.Manifold.Riemannian. riemannianVolumeMeasure_isFiniteMeasureOnCompacts: the Riemannian Hausdorff-volume measure is finite on compact sets.
• RellichKondrachov.Geometry.Manifold.Riemannian.riemannianVolumeMeasure_isFiniteMeasure: on a compact manifold, the total volume is finite.

@[implicit_reducible]

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

Borel σ-algebra on the model space E.

Equations

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

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

theorem RellichKondrachov.Geometry.Manifold.Riemannian.riemannianVolumeMeasure_isFiniteMeasureOnCompacts {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ 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.IsFiniteMeasureOnCompacts (riemannianVolumeMeasure I)

theorem RellichKondrachov.Geometry.Manifold.Riemannian.riemannianVolumeMeasure_isFiniteMeasure {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ 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] [CompactSpace M] : MeasureTheory.IsFiniteMeasure (riemannianVolumeMeasure I)