Riemannian volume density in a chart

The local Riemannian volume density is the positive square root of the determinant of the metric Gram matrix. Under a C^n metric on a C^(n+1) manifold, it is C^n on its chart and transforms by the absolute determinant of a change of frame. Thus it applies without an orientation, including on manifolds with boundary.

The frame is Riemannian.Tensor.chartLocalFrame, based on Module.finBasis ℝ E. Accordingly the coordinate measure to be weighted by this density is the Haar measure normalized by that basis. No orthonormality of the model-space basis is assumed. This file supplies the local density and its transition rule; it does not assemble a measure on the manifold.

The convention follows J. M. Lee, Introduction to Riemannian Manifolds, 2nd ed., Springer GTM 176 (2018), Propositions 2.41 and 2.44.

noncomputable def TauCeti.chartVolumeDensity {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] (α x : M) : ℝ

The Riemannian volume density in the frame of the chart centred at α, relative to the model-space basis Module.finBasis ℝ E.

Equations

• TauCeti.chartVolumeDensity α x = √(Riemannian.Tensor.chartGramMatrix α x).det

theorem TauCeti.chartVolumeDensity_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] [ChartedSpace H M] [IsManifold I 1 M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] (α x : M) : chartVolumeDensity α x = √(Riemannian.Tensor.chartGramMatrix α x).det

The coordinate formula for Riemannian volume density.

theorem TauCeti.chartVolumeDensity_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] [ChartedSpace H M] [IsManifold I 1 M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] (α x : M) : 0 ≤ chartVolumeDensity α x

The chart density is nonnegative, including at its values outside the chart.

theorem TauCeti.chartVolumeDensity_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] [ChartedSpace H M] [IsManifold I 1 M] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] (α : M) {x : M} (hx : x ∈ (trivializationAt E (TangentSpace I) α).baseSet) : 0 < chartVolumeDensity α x

The chart density is strictly positive on the chart domain.

@[simp]

theorem TauCeti.chartVolumeDensity_sq {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] (α x : M) : chartVolumeDensity α x ^ 2 = (Riemannian.Tensor.chartGramMatrix α x).det

Squaring the density recovers the Gram determinant, including outside the chart domain.

theorem TauCeti.contMDiffOn_chartVolumeDensity {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] {n : WithTop ℕ∞} [IsManifold I (n + 1) M] [IsContMDiffRiemannianBundle I n E fun (x : M) => TangentSpace I x] (α : M) : ContMDiffOn I (modelWithCornersSelf ℝ ℝ) n (chartVolumeDensity α) (trivializationAt E (TangentSpace I) α).baseSet

A C^n metric has a C^n volume density in every chart of a C^(n+1) manifold.

theorem TauCeti.chartVolumeDensity_changeFrame {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] (α β : M) {x : M} (hα : x ∈ (trivializationAt E (TangentSpace I) α).baseSet) (hβ : x ∈ (trivializationAt E (TangentSpace I) β).baseSet) : chartVolumeDensity α x = |(((trivializationAt E (TangentSpace I) β).basisAt (Module.finBasis ℝ E) hβ).toMatrix ⇑((trivializationAt E (TangentSpace I) α).basisAt (Module.finBasis ℝ E) hα)).det| * chartVolumeDensity β x

Changing from the frame at β to the frame at α multiplies the volume density by the absolute determinant of the frame-coordinate matrix. The absolute value makes the rule valid for orientation-reversing transitions as well.