Riemannian volume in a chart

A continuous Riemannian metric determines a measure locally by weighting coordinate Lebesgue measure with the positive square root of the metric Gram determinant. This file constructs that measure on the source of each preferred manifold chart and proves that the resulting measures agree on chart overlaps. The compatibility theorem is the descent input for assembling the Riemannian volume measure on the whole manifold.

The coordinate Lebesgue measure is Module.finBasis ℝ E |>.addHaar, matching the basis used by TauCeti.chartVolumeDensity. The overlap proof applies Mathlib's change-of-variables theorem to the extended chart transition and uses TauCeti.chartVolumeDensity_symm_apply_changeChart_fderivWithin for its Jacobian factor.

The construction works without an orientation and for manifolds with boundary or corners. It follows J. M. Lee, Introduction to Riemannian Manifolds, 2nd ed., Springer GTM 176 (2018), Proposition 2.44.

Main definitions

• TauCeti.chartRiemannianVolume: the Riemannian volume measure supplied by one preferred chart.

Main results

• TauCeti.chartRiemannianVolume_apply: the coordinate integral formula.
• TauCeti.chartRiemannianVolume_restrict_source: a chart volume is supported on its source.
• TauCeti.chartRiemannianVolume_finiteAtFilter_nhds: every point of a chart source has a neighbourhood of finite chart volume.
• TauCeti.chartRiemannianVolume_restrict_overlap: chart volume measures agree on overlaps.

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

The local Riemannian volume measure supplied by the preferred chart at α. It is supported on the source of that chart.

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.chartRiemannianVolume_apply {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] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContinuousRiemannianBundle E fun (x : M) => TangentSpace I x] (α : M) {s : Set M} (hs : MeasurableSet s) : (chartRiemannianVolume α) s = ∫⁻ (y : E) in ↑(extChartAt I α) '' (s ∩ (extChartAt I α).source), ENNReal.ofReal (chartVolumeDensity α (↑(extChartAt I α).symm y)) ∂(Module.finBasis ℝ E).addHaar

A chart volume measure evaluates a measurable set by integrating the chart density over its coordinate image inside the chart source.

@[simp]

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

A chart volume measure is supported on the source of its chart.

theorem TauCeti.chartRiemannianVolume_finiteAtFilter_nhds {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] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContinuousRiemannianBundle E fun (x : M) => TangentSpace I x] (α : M) {x : M} (hx : x ∈ (chartAt H α).source) : (chartRiemannianVolume α).FiniteAtFilter (nhds x)

Every point of a chart source has a neighbourhood of finite chart volume. The chart volume need not be locally finite at the frontier of the chart source, where the density may blow up.

theorem TauCeti.chartRiemannianVolume_restrict_overlap {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] [Bundle.RiemannianBundle fun (x : M) => TangentSpace I x] [IsContinuousRiemannianBundle E fun (x : M) => TangentSpace I x] (α β : M) : (chartRiemannianVolume α).restrict ((extChartAt I α).source ∩ (extChartAt I β).source) = (chartRiemannianVolume β).restrict ((extChartAt I α).source ∩ (extChartAt I β).source)

The local Riemannian volume measures supplied by two preferred charts agree on their overlap. This is the cocycle condition needed to descend the local coordinate measures to the manifold.