The Riemannian volume measure

A continuous Riemannian metric on a manifold M determines a measure on M: in each chart it is coordinate Lebesgue measure weighted by the square root of the metric Gram determinant, the local measure TauCeti.chartRiemannianVolume. These local measures agree on chart overlaps, so when countably many chart sources cover M (for instance when M is second countable, or σ-compact) they glue to a unique measure on the Borel σ-algebra of M, TauCeti.riemannianVolume I M.

The construction needs no orientation and applies to manifolds with boundary or corners. The Riemannian volume is locally finite, so it is a finite measure on a compact manifold; this is the measure against which the total volume of a closed Riemannian manifold is taken.

The construction follows J. M. Lee, Introduction to Riemannian Manifolds, 2nd ed., Springer GTM 176 (2018), Proposition 2.44 and the discussion of the Riemannian density following it.

Main definitions

• TauCeti.riemannianVolume: the Riemannian volume measure of a manifold with a continuous Riemannian metric.

Main results

• TauCeti.riemannianVolume_restrict_source: on the source of each preferred chart, the Riemannian volume is the chart volume.
• TauCeti.eq_riemannianVolume_iff: this property characterizes the Riemannian volume.
• TauCeti.riemannianVolume_apply_of_subset: the volume of a subset of a chart source is its chart volume.
• TauCeti.isLocallyFiniteMeasure_riemannianVolume: the Riemannian volume is locally finite.

noncomputable def TauCeti.riemannianVolume {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] [MeasurableSpace M] [BorelSpace M] [LindelofSpace M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContinuousRiemannianBundle E fun (x : M) => TangentSpace I x] : MeasureTheory.Measure M

The Riemannian volume measure of a manifold M with a continuous Riemannian metric: the unique measure whose restriction to the source of each preferred chart is the chart volume TauCeti.chartRiemannianVolume, coordinate Lebesgue measure weighted by the square root of the metric Gram determinant. It is characterized by TauCeti.eq_riemannianVolume_iff.

Equations

• TauCeti.riemannianVolume I M = ⋯.choose

@[simp]

theorem TauCeti.riemannianVolume_restrict_source {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] [MeasurableSpace M] [BorelSpace M] [LindelofSpace M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContinuousRiemannianBundle E fun (x : M) => TangentSpace I x] (α : M) : (riemannianVolume I M).restrict (chartAt H α).source = chartRiemannianVolume α

On the source of each preferred chart, the Riemannian volume is the chart volume.

theorem TauCeti.eq_riemannianVolume_iff {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] [MeasurableSpace M] [BorelSpace M] [LindelofSpace M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContinuousRiemannianBundle E fun (x : M) => TangentSpace I x] {ν : MeasureTheory.Measure M} : ν = riemannianVolume I M ↔ ∀ (α : M), ν.restrict (chartAt H α).source = chartRiemannianVolume α

The Riemannian volume is the only measure agreeing with the chart volume on the source of every preferred chart.

theorem TauCeti.riemannianVolume_apply_of_subset {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] [MeasurableSpace M] [BorelSpace M] [LindelofSpace M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContinuousRiemannianBundle E fun (x : M) => TangentSpace I x] {α : M} {s : Set M} (hs : s ⊆ (chartAt H α).source) : (riemannianVolume I M) s = (chartRiemannianVolume α) s

The Riemannian volume of a subset of a chart source is its chart volume.

instance TauCeti.isLocallyFiniteMeasure_riemannianVolume {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] [MeasurableSpace M] [BorelSpace M] [LindelofSpace M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContinuousRiemannianBundle E fun (x : M) => TangentSpace I x] : MeasureTheory.IsLocallyFiniteMeasure (riemannianVolume I M)

The Riemannian volume is locally finite: every point has a neighbourhood of finite volume. In particular, the Riemannian volume of a compact manifold is a finite measure.