Total Riemannian volume

The Riemannian volume measure of a compact manifold has finite mass. Its total mass is therefore a real number, TauCeti.riemannianTotalVolume. This is the volume associated to the chosen Riemannian metric, and is preserved by differentiable isometries. The construction also applies to compact manifolds with boundary or corners.

The volume is the total mass of the Riemannian density of J. M. Lee, Introduction to Riemannian Manifolds, 2nd ed., Springer GTM 176 (2018), Chapter 2.

The RiemannianIsometry namespace packages measure and total-volume invariance at the bundled isometry API.

noncomputable def TauCeti.riemannianTotalVolume {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] (I : ModelWithCorners ℝ E H) (M : Type u_4) [TopologicalSpace M] [CompactSpace M] [ChartedSpace H M] [IsManifold I 1 M] [MeasurableSpace M] [BorelSpace M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContinuousRiemannianBundle E fun (x : M) => TangentSpace I x] : ℝ

The total volume of a compact Riemannian manifold, as a real number.

theorem TauCeti.riemannianTotalVolume_def {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] [CompactSpace M] [ChartedSpace H M] [IsManifold I 1 M] [MeasurableSpace M] [BorelSpace M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContinuousRiemannianBundle E fun (x : M) => TangentSpace I x] : riemannianTotalVolume I M = (riemannianVolume I M).real Set.univ

Total Riemannian volume is the real mass of the whole manifold.

@[simp]

theorem TauCeti.ofReal_riemannianTotalVolume {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] [CompactSpace M] [ChartedSpace H M] [IsManifold I 1 M] [MeasurableSpace M] [BorelSpace M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContinuousRiemannianBundle E fun (x : M) => TangentSpace I x] : ENNReal.ofReal (riemannianTotalVolume I M) = (riemannianVolume I M) Set.univ

The total volume recovers the finite mass of the Riemannian volume measure.

theorem TauCeti.riemannianTotalVolume_nonneg {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] [CompactSpace M] [ChartedSpace H M] [IsManifold I 1 M] [MeasurableSpace M] [BorelSpace M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContinuousRiemannianBundle E fun (x : M) => TangentSpace I x] : 0 ≤ riemannianTotalVolume I M

Total Riemannian volume is nonnegative.

theorem TauCeti.riemannianTotalVolume_pos {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] [CompactSpace M] [ChartedSpace H M] [IsManifold I 1 M] [MeasurableSpace M] [BorelSpace M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContinuousRiemannianBundle E fun (x : M) => TangentSpace I x] [Nonempty M] : 0 < riemannianTotalVolume I M

A nonempty compact Riemannian manifold has positive total volume.

theorem Homeomorph.riemannianTotalVolume_eq {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] [CompactSpace M] [ChartedSpace H M] [IsManifold I 1 M] [MeasurableSpace M] [BorelSpace M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContinuousRiemannianBundle E fun (x : M) => TangentSpace I x] {H' : Type u_4} [TopologicalSpace H'] {I' : ModelWithCorners ℝ E H'} {N : Type u_5} [TopologicalSpace N] [CompactSpace N] [ChartedSpace H' N] [IsManifold I' 1 N] [MeasurableSpace N] [BorelSpace N] [Bundle.RiemannianBundle fun (y : N) => TangentSpace I' y] [IsContinuousRiemannianBundle E fun (y : N) => TangentSpace I' y] (Φ : M ≃ₜ N) (hΦ : MDiff ⇑Φ) (hinner : ∀ (x : M) (v w : TangentSpace I x), inner ℝ ((mfderiv% ⇑Φ x) v) ((mfderiv% ⇑Φ x) w) = inner ℝ v w) : TauCeti.riemannianTotalVolume I M = TauCeti.riemannianTotalVolume I' N

A differentiable isometry between compact Riemannian manifolds preserves total volume.

theorem TauCeti.RiemannianIsometry.riemannianTotalVolume_eq {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] [CompactSpace M] [ChartedSpace H M] [IsManifold I 1 M] [MeasurableSpace M] [BorelSpace M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContinuousRiemannianBundle E fun (x : M) => TangentSpace I x] {H' : Type u_6} [TopologicalSpace H'] {J : ModelWithCorners ℝ E H'} {N : Type u_7} [TopologicalSpace N] [CompactSpace N] [ChartedSpace H' N] [IsManifold J 1 N] [MeasurableSpace N] [BorelSpace N] [Bundle.RiemannianBundle fun (y : N) => TangentSpace J y] [IsContinuousRiemannianBundle E fun (y : N) => TangentSpace J y] (Φ : RiemannianIsometry I J M N) : riemannianTotalVolume I M = riemannianTotalVolume J N

A Riemannian isometry between compact manifolds preserves total Riemannian volume.