Change of coordinates for Riemannian volume density

The Riemannian volume density in a chart transforms by the absolute Jacobian determinant of a change of coordinates. This file identifies the frame-change matrix in TauCeti.chartVolumeDensity_changeFrame with the matrix of Mathlib's tangent coordinate change, then states the resulting coordinate formula and its coordinate-domain form.

These formulas are the compatibility needed to assemble the chart densities into a measure on a manifold. They apply to manifolds with boundary and corners: derivatives are taken within the range of the model with corners, exactly as in Mathlib's tangent-bundle construction.

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

Main results

• TauCeti.chartVolumeDensity_changeChart: the volume density transforms by the absolute determinant of the tangent coordinate change.
• TauCeti.chartVolumeDensity_symm_apply_changeChart_fderivWithin: the coordinate-domain form used by change-of-variables arguments.

theorem TauCeti.chartVolumeDensity_changeChart {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 = |(tangentCoordChange I α β x).det| * chartVolumeDensity β x

On the overlap of two charts, the Riemannian volume density in the source chart is the density in the target chart multiplied by the absolute determinant of the tangent coordinate change.

theorem TauCeti.chartVolumeDensity_symm_apply_changeChart_fderivWithin {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) {y : E} (hy : y ∈ ((extChartAt I α).symm.trans (extChartAt I β)).source) : chartVolumeDensity α (↑(extChartAt I α).symm y) = |(fderivWithin ℝ (↑(extChartAt I β) ∘ ↑(extChartAt I α).symm) (Set.range ↑I) y).det| * chartVolumeDensity β (↑(extChartAt I α).symm y)

The coordinate-domain form of the density transition law. At a point in the source of the extended change from the α chart to the β chart, the source density pulled back by the inverse α chart is the target density multiplied by the absolute Jacobian determinant.