The Riemannian volume of a metric on a manifold, from chart Gram densities #

The namespace is MetricFamily, not RiemannianMetric: Mathlib has a structure of that name (Mathlib/Topology/VectorBundle/Riemannian.lean, with ContMDiffRiemannianMetric beside it), and this file works with a bare family g : ∀ x, T_x → T_x → ℝ plus IsBilinear; the volume of Mathlib's bundled metrics is the section "Mathlib's Riemannian metrics" at the end. Category: 1-Mathlib (measure theory on manifolds: the Riemannian volume measure of a metric family, absent from Mathlib at the pin — Mathlib/Geometry/Manifold/VectorBundle/Riemannian.lean has Riemannian bundles, no volume; G17 of the generator-layer plan §9).

A Riemannian metric g on a manifold M modelled on E has, in the chart at x₀, the Gram matrix G_{x₀}(w)ᵢⱼ = g (symmL (eᵢ)) (symmL (eⱼ)) against a basis e of E (the metric at the point under w, read through the tangent trivialisation), and its Riemannian volume has the chart density √det G_{x₀}(w). This module builds the measure exactly as TopFormMeasure.lean builds the measure of a top form — chart densities glued along the measurable partition of a ChartCover — with the Gram density in place of the top-form coefficient.

MetricFamily.localRep g x₀ w u v — the local representative of the metric family in the chart at x₀;
MetricFamily.gram e g x₀ w — its Gram matrix against e;
MetricFamily.chartDensity e g x₀ w = ENNReal.ofReal √det — the Riemannian chart density;
MetricFamily.chartMeasure μ e g x₀ — the density measure on the chart's target, pushed to M by the chart (chartMeasure_apply);
★★ MetricFamily.riemannianVolume μ e g c — the Riemannian volume of g, glued along the cover c;
★★ MetricFamily.riemannianVolume_eq_smul_topFormMeasure — if in every chart of the cover the Gram density is k times the coefficient density of a top form, the Riemannian volume is k times the top-form measure. This is the bridge the Kähler identity vol_g = ω^{∧n}/n! uses on ℂℙⁿ (Instances/ProjectiveSpaceFubiniStudyRiemannian.lean);
Q30 / G17b (2026-09-11). For a bilinear family (IsBilinear g, the four pointwise equations): localRep_transition (the local representative pulls back along the transition's derivative), ★ chartDensity_transition (the Jacobian rule for Gram densities, √det G_{x₀} = |det Dφ| · √det G_y ∘ φ, from the congruence Aᵀ G A and det_transpose), ★★ chartMeasure_congr (chart-independence, by change of variables), and ★★ riemannianVolume_congr_cover — the Riemannian volume is canonical: it does not depend on the chart cover. The proofs are those of TopFormMeasure.lean with the Gram rule in place of the top-form coefficient rule.

Honest scope #

⚠️ Chart-independence needs bilinearity, and asks for it. The definitions take a bare family g so that they ask nothing; chartMeasure_congr and riemannianVolume_congr_cover take IsBilinear g (pointwise bilinearity, the four equations), which is what the Gram congruence Aᵀ G A uses and all a metric has. No symmetry or positivity is asked; a family with a non-positive Gram determinant has chart density 0 there and the theorems still hold.

⚠️ g is a family, not a section. No smoothness or symmetry of g is assumed by the definitions; a non-positive Gram determinant gives density 0 (Real.sqrt of a negative is 0). The ℂℙⁿ instance supplies a genuine metric (isBilinear_fsMetric). Not stated: that an isometry preserves riemannianVolume (the twin of topFormMeasure_map_eq; same route, no consumer).

Provenance and references. The generator-layer plan (G17); Geometry/Manifold/TopFormMeasure.lean (the construction mirrored); Instances/ProjectiveSpaceFubiniStudyRiemannian.lean (the instance).

The Riemannian volume of a metric on a manifold, from chart Gram densities #

Honest scope #

Chart-independence (Q30 / G17b) #

The basis' own Haar measure: the Riemannian volume is canonical #

Mathlib's Riemannian metrics #