Splitting off one coordinate of an infinite product measure

For a family of probability measures indexed by Option ι, the product measure Measure.infinitePi μ is the law of an assignment x whose coordinates are independent with laws μ i. Reading x as its value at none together with its restriction to the indices some i separates it into two independent pieces, so

(Measure.infinitePi μ).map (fun x => (x none, fun i => x (some i)))
  = μ none ⊗ Measure.infinitePi (fun i => μ (some i)).

This is the infinite-product analogue of Mathlib's MeasureTheory.Measure.pi_map_piOptionEquivProd, which is stated for Measure.pi over a finite index type. It isolates one distinguished coordinate — a global or initial variable — from the independent remaining coordinates, each with its respective law.

Main results

• TauCeti.MeasureTheory.Measure.infinitePi_map_none_some — the displayed identity.

@[simp]

theorem TauCeti.MeasureTheory.Measure.infinitePi_map_none_some {ι : Type u_1} {X : Option ι → Type u_2} [(i : Option ι) → MeasurableSpace (X i)] (μ : (i : Option ι) → MeasureTheory.Measure (X i)) [∀ (i : Option ι), MeasureTheory.IsProbabilityMeasure (μ i)] : MeasureTheory.Measure.map (fun (x : (i : Option ι) → X i) => (x none, fun (i : ι) => x (some i))) (MeasureTheory.Measure.infinitePi μ) = (μ none).prod (MeasureTheory.Measure.infinitePi fun (i : ι) => μ (some i))

Splitting off the coordinate none of an infinite product measure. Under the product of probability measures indexed by Option ι, the coordinate at none and the family of coordinates at some i are independent, with laws μ none and the product of the μ (some i).