The measure of a top-degree form on a manifold #

Category: 1-Mathlib (CSD-free; upstream target Mathlib.Geometry.Manifold, where no measure or integration on manifolds exists at the pin — Riemannian/Basic.lean imports measure theory for path lengths only).

A form whose degree is a basis index type of the model space has, in every chart, a density — the absolute value of its coefficient against the basis — and those densities glue to a measure on the manifold.

DifferentialForm.chartDensity e s x₀ w — |coefficient of the local representative of s in the chart at x₀, at w|, as an ℝ≥0∞;
DifferentialForm.chartMeasure μ e s x₀ — the density measure on the chart's target (against a Haar measure μ on the model), pushed to M by the chart; chartMeasure_apply reads it as an integral over the chart image;
★★ DifferentialForm.chartMeasure_congr — chart-independence: on a measurable set inside two chart domains the two chart measures agree. Change of variables along the chart transition (MeasureTheory.lintegral_image_eq_lintegral_abs_det_fderiv_mul), whose Jacobian is exactly the factor by which the coefficient of a top form transforms (compContinuousLinearMap_apply_basis through localRep_transition). This is the whole content of "a top form is a density";
ChartCover E M — a finite cover of M by chart domains, as data (m base points), with the measurable partition piece i subordinate to it (measurableSet_piece, pairwise_disjoint_piece, iUnion_piece);
★★ DifferentialForm.topFormMeasure μ e s c — the measure of a top form: the chart measures glued along the partition;
★★ topFormMeasure_apply_of_subset_source — on a measurable set inside any chart domain (not only the cover's) the glued measure is that chart's measure; hence ★ topFormMeasure_congr_cover — the measure does not depend on the cover;
★ topFormMeasure_addHaar_basis — against the basis' own Haar measure e.addHaar it does not depend on the basis either (apply_basis_eq_mul_det, addHaar_basis_eq_smul): the measure of a top form is canonical;
★ chartMeasure_preimage_eq and ★★ topFormMeasure_map_eq — invariance: a homeomorphism whose chart expressions are differentiable and pull the local representative at the target chart back to the local representative at the source chart preserves the measure (differentiability, not smoothness, is what the change of variables uses; the Hamiltonian flow of HamiltonianFlowVolume.lean supplies exactly that). The proof is chart-independence with the chart transition replaced by the map's chart expression, summed over the double partition by the cover's pieces and their images;
★ isLocallyFiniteMeasure_topFormMeasure, ★ isFiniteMeasure_topFormMeasure — the measure of a smooth top form is locally finite (a compact ball inside a chart has finite measure, the density being continuous there), hence finite on a compact manifold;
★ topFormMeasure_ne_zero_of_localRep_ne_zero (the generic half) — a smooth top form whose coefficient against the basis does not vanish at one chart point has nonzero measure: the density is continuous, so bounded below on a ball, and Haar measure gives balls positive measure (continuous_eval_const: evaluation on a fixed family is Lipschitz).

Honest scope #

⚠️ A finite atlas given as data. Compact manifolds have one, and ℂℙⁿ's affine atlas is one (Instances/ProjectiveSpaceChartCover.lean); nothing here handles an infinite atlas, and no partition of unity is used — the gluing is along a measurable partition, which is why the construction needs no paracompactness and no bump functions.

⚠️ Densities, not integrals of forms. The measure uses |coefficient|; no orientation is chosen and none is needed. Integrating a form with its sign is not defined here.

⚠️ Invariance, not general naturality. topFormMeasure_map_eq is stated for a map that preserves the form in charts (the hypothesis is the chart form of "g^* s = s"); the general statement measureOf (g^* s) = map g⁻¹ (measureOf s) would need the pullback of forms along maps of manifolds, which is not built. Non-vanishing of a particular measure reduces to one chart coefficient at one point (topFormMeasure_ne_zero_of_localRep_ne_zero); computing that coefficient is consumer-side.

⚠️ ∞ and 𝓘(ℝ, E) only, inherited from ExteriorDerivative.lean; the model E is finite-dimensional real, Borel, with an additive Haar measure supplied as an argument.

Provenance and references. The top-power plan (M3); Analysis/Normed/Module/Alternating/TopForm.lean (M1, the Jacobian rule); Geometry/Manifold/ExteriorDerivative.lean (localRep, localRep_transition, contDiffAt_chart_transition); Mathlib/MeasureTheory/Function/Jacobian.lean; the completed-work ledger.

The measure of a top-degree form on a manifold #

Honest scope #

Finite chart covers and their measurable partitions #

Evaluation on a fixed family is continuous #

Chart densities and chart measures #

The glued measure #

Invariance under a form-preserving homeomorphism #

The basis' own Haar measure: the measure of a top form is canonical #

Local finiteness, and positivity #