The Riemannian volume of a metric-indexed copy

The copy TauCeti.WithMetric g of a manifold M carries the metric g as its RiemannianBundle instance, and the tautological map ofWithMetric : WithMetric g → M is an isometry onto M with g installed as its fibre metric. By the isometry invariance of the Riemannian volume, this map carries the volume of the copy to the volume of (M, g), so integrals against the volume of WithMetric g are integrals against the volume of g on M itself.

This lets results proved for the installed metric of a manifold, such as the divergence theorem and Green's identities, be applied to the volumes of the copies, which are used to compare two metrics on M without installing both on the same carrier.

Main results

• TauCeti.WithMetric.measurePreserving_ofWithMetric: ofWithMetric carries the volume of WithMetric g to the volume of M with g installed.
• TauCeti.WithMetric.integral_comp_ofWithMetric: ∫ φ ∘ ofWithMetric against the volume of WithMetric g is ∫ φ against the volume of g on M.

theorem TauCeti.WithMetric.measurePreserving_ofWithMetric {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {n : WithTop ℕ∞} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] [MeasurableSpace M] [BorelSpace M] [LindelofSpace M] (g : Bundle.ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x) : MeasureTheory.MeasurePreserving ofWithMetric (riemannianVolume I (WithMetric g)) (riemannianVolume I M)

The volume of a metric-indexed copy. The tautological map ofWithMetric carries the Riemannian volume of WithMetric g to the Riemannian volume of M with g installed as its fibre metric.

theorem TauCeti.WithMetric.integral_comp_ofWithMetric {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {H : Type u_2} [TopologicalSpace H] {I : ModelWithCorners ℝ E H} {n : WithTop ℕ∞} {M : Type u_3} [TopologicalSpace M] [ChartedSpace H M] [IsManifold I 1 M] [MeasurableSpace M] [BorelSpace M] [LindelofSpace M] (g : Bundle.ContMDiffRiemannianMetric I n E fun (x : M) => TangentSpace I x) {F : Type u_4} [NormedAddCommGroup F] [NormedSpace ℝ F] (φ : M → F) : ∫ (x : WithMetric g), φ x.ofWithMetric ∂riemannianVolume I (WithMetric g) = ∫ (x : M), φ x ∂riemannianVolume I M

Integration against the volume of the metric-indexed copy WithMetric g is integration against the volume of g on M: ∫ φ ∘ ofWithMetric dV_{WithMetric g} = ∫ φ dV_g.