Mathlib upstream candidate: Measure.pi is preserved by currying a product index

MeasurableEquiv.piCurry regroups a product over a sigma index Σ i, κ i into an iterated product ((i : ι) → (j : κ i) → X i j). Mathlib proves it measurable (measurable_piCurry) but provides no measure-preserving statement: currying a Measure.pi over Σ i, κ i yields the iterated Measure.pi-of-Measure.pi,

map (piCurry X) (Measure.pi μ) = Measure.pi (fun i => Measure.pi (fun j => μ ⟨i, j⟩)).

The proof is the sigma-index analogue of measurePreserving_arrowProdEquivProdArrow: verify on the box-of-boxes π-system (pi_eq_generateFrom), where piCurry⁻¹ of a box of boxes is a genuine sigma-box, so Measure.pi_pi factors both sides and Finset.prod_sigma' collapses the double product to the sigma product.

Category: 1-Mathlib (CSD-free; staged as a Mathlib upstream candidate).

Provenance

Needed for the general-N Duistermaat–Heckman / Dirichlet computation (CsdLean4/LF4/MomentRatioUniformN.lean + the Slice E assembly): the standard Gaussian on ℝ^{N×2} (indexed by the product Fin N × Fin 2) must be regrouped into a product over Fin N of ℝ²-Gaussians before Slices C/D apply. See specs/general-n-dh-plan.md Slice E.

Tags

measure preserving, pi, curry, sigma, product measure

theorem MeasureTheory.measurePreserving_piCurry {ι : Type u_1} [Fintype ι] {κ : ι → Type u_2} [(i : ι) → Fintype (κ i)] {X : (i : ι) → κ i → Type u_3} [(i : ι) → (j : κ i) → MeasurableSpace (X i j)] (μ : (p : (i : ι) × κ i) → Measure (X p.fst p.snd)) [∀ (p : (i : ι) × κ i), SigmaFinite (μ p)] : MeasurePreserving (⇑(MeasurableEquiv.piCurry X)) (Measure.pi μ) (Measure.pi fun (i : ι) => Measure.pi fun (j : κ i) => μ ⟨i, j⟩)

Currying a product index preserves Measure.pi. The measurable equivalence MeasurableEquiv.piCurry (regrouping Σ i, κ i into an iterated index) pushes the product measure forward to the iterated product measure.

Product-index variant

The concrete form consumed by the general-N Duistermaat–Heckman assembly: the standard Gaussian on ℝ^{N×2} is indexed by the product Fin N × Fin 2, so the regrouping needed there is currying a product index, not a sigma index. The proof is identical to measurePreserving_piCurry with Fintype.prod_prod_type (product big operator) in place of Finset.prod_sigma'.

theorem MeasureTheory.map_curryProd_pi {ιp : Type u_4} {κp : Type u_5} [Fintype ιp] [Fintype κp] {α : ιp × κp → Type u_6} [(p : ιp × κp) → MeasurableSpace (α p)] (ν : (p : ιp × κp) → Measure (α p)) [∀ (p : ιp × κp), SigmaFinite (ν p)] : Measure.map (fun (y : (p : ιp × κp) → α p) (i : ιp) (j : κp) => y (i, j)) (Measure.pi ν) = Measure.pi fun (i : ιp) => Measure.pi fun (j : κp) => ν (i, j)

Currying a product index preserves Measure.pi. The plain currying map y ↦ fun i j => y (i, j) pushes the product measure over ιp × κp forward to the iterated product measure.