Coordinate projections of finite product measures

This file records measure-preserving coordinate projections and refreshes for finite product measures.

Projecting along an embedding. If e : ι ↪ κ, restriction of a product-distributed assignment on κ to the coordinates in the image of e has the corresponding product law on ι. This is the finite-family form of the fact that a subfamily of independent coordinates is still independent.

Reading off a pair of coordinates. The evaluation map x ↦ (x a, x b) at two distinct indices pushes Measure.pi μ forward to μ a ⊗ μ b: distinct coordinates of a product measure are independent, and each single coordinate has law μ a (Mathlib's measurePreserving_eval). This is the two-variable companion of measurePreserving_eval, and is what transports an almost-everywhere statement about a pair back to the product space.

Splitting off one coordinate. Mathlib's Equiv.piSplitAt pushes Measure.pi μ forward to μ i₀ ⊗ Measure.pi fun j : {i // i ≠ i₀} ↦ μ j. Mathlib splits a product measure along a predicate and leaves both halves as products over subtypes; a construction that singles out one index wants the one-element half collapsed to the factor itself.

Refreshing a pair of coordinates. Overwriting two distinct probability coordinates by an independent pair samples the same law: the map

(z, s, t) ↦ Function.update (Function.update z a s) b t

pushes (Measure.pi μ) ⊗ (μ a ⊗ μ b) forward to Measure.pi μ. The two overwritten coordinates carry the fresh samples and the remaining coordinates keep the ones they had, which is the product law again.

For a = b the pair degenerates to a single refresh because the second update overwrites the first. The distinctness hypothesis records the two-slot factorisation needed by consumers of this construction.

Main statements

• TauCeti.measurePreserving_pi_comp_embedding — restricting a product assignment along an embedding is measure preserving;
• TauCeti.measurePreserving_eval_pair — reading off two distinct coordinates is measure preserving;
• TauCeti.measurePreserving_piSplitAt — separating the coordinate i₀ from the rest is measure preserving;
• TauCeti.measurePreserving_update_update — the two-coordinate refresh is measure preserving.

Implementation

measurePreserving_eval_pair reads the pair law off Mathlib's independence of the coordinates of a product measure, ProbabilityTheory.iIndepFun_pi, through ProbabilityTheory.indepFun_iff_map_prod_eq_prod_map_map.

The proof of measurePreserving_update_update splits the product into the coordinates {a, b} and their complement using Mathlib's measure-preserving product equivalences. The fresh pair replaces the selected coordinates, while the complementary coordinates are projected from the original assignment; recombining the two parts is pointwise the double update.

theorem TauCeti.measurePreserving_pi_comp_embedding {ι : Type u_1} {κ : Type u_2} [Fintype ι] [Fintype κ] {α : κ → Type u_3} [(j : κ) → MeasurableSpace (α j)] (μ : (j : κ) → MeasureTheory.Measure (α j)) [∀ (j : κ), MeasureTheory.IsProbabilityMeasure (μ j)] (e : ι ↪ κ) : MeasureTheory.MeasurePreserving (fun (x : (j : κ) → α j) (i : ι) => x (e i)) (MeasureTheory.Measure.pi μ) (MeasureTheory.Measure.pi fun (i : ι) => μ (e i))

Restricting a finite product-distributed assignment along an embedding of index types is measure preserving. The target product uses exactly the marginals selected by the embedding.

theorem TauCeti.measurePreserving_eval_pair {ι : Type u_1} [Fintype ι] {α : ι → Type u_2} [(i : ι) → MeasurableSpace (α i)] (μ : (i : ι) → MeasureTheory.Measure (α i)) [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)] {a b : ι} (hab : a ≠ b) : MeasureTheory.MeasurePreserving (fun (x : (i : ι) → α i) => (x a, x b)) (MeasureTheory.Measure.pi μ) ((μ a).prod (μ b))

Two distinct coordinates of a product measure carry the product of their laws. Reading off the coordinates a ≠ b of a product-distributed assignment pushes Measure.pi μ forward to μ a ⊗ μ b.

The one-coordinate statement is Mathlib's MeasureTheory.measurePreserving_eval; distinctness is what makes the pair independent, and hence its law a product.

theorem TauCeti.measurePreserving_piSplitAt {ι : Type u_1} [Fintype ι] [DecidableEq ι] {α : ι → Type u_2} [(i : ι) → MeasurableSpace (α i)] (μ : (i : ι) → MeasureTheory.Measure (α i)) [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)] (i₀ : ι) : MeasureTheory.MeasurePreserving (⇑(Equiv.piSplitAt i₀ α)) (MeasureTheory.Measure.pi μ) ((μ i₀).prod (MeasureTheory.Measure.pi fun (j : { i : ι // i ≠ i₀ }) => μ ↑j))

Splitting off one coordinate of a finite product measure. Mathlib's Equiv.piSplitAt, which reads a product-distributed assignment as its value at i₀ paired with its values at the remaining indices, pushes Measure.pi μ forward to μ i₀ ⊗ Measure.pi fun j : {i // i ≠ i₀} => μ j.

This is Mathlib's MeasureTheory.measurePreserving_piEquivPiSubtypeProd for the predicate (· = i₀), with the one-element factor collapsed to μ i₀.

theorem TauCeti.measurePreserving_update_update {ι : Type u_1} [Fintype ι] [DecidableEq ι] {α : ι → Type u_2} [(i : ι) → MeasurableSpace (α i)] (μ : (i : ι) → MeasureTheory.Measure (α i)) [∀ (i : ι), MeasureTheory.SigmaFinite (μ i)] {a b : ι} [MeasureTheory.IsProbabilityMeasure (μ a)] [MeasureTheory.IsProbabilityMeasure (μ b)] (hab : a ≠ b) : MeasureTheory.MeasurePreserving (fun (w : ((i : ι) → α i) × α a × α b) => Function.update (Function.update w.1 a w.2.1) b w.2.2) ((MeasureTheory.Measure.pi μ).prod ((μ a).prod (μ b))) (MeasureTheory.Measure.pi μ)

Overwriting the two distinct coordinates a and b of a product-distributed assignment by an independent pair leaves the product law unchanged.