Splitting one coordinate off a finite product measure

Mathlib splits a coordinate off Measure.pi only for index type Fin (n + 1) (measurePreserving_piFinSuccAbove). This file gives the same tower for Equiv.piSplitAt, which works over any finite index type: the measurable equivalence and the statement that it carries Measure.pi μ to (μ i).prod (Measure.pi fun j : {j // j ≠ i} ↦ μ j). With Measure.prod_apply and Measure.pi_pi this computes probabilities that tie the other coordinates to the i-th.

Main definitions

• MeasurableEquiv.piSplitAt: the measurable version of Equiv.piSplitAt.

Main results

• MeasureTheory.measurePreserving_piSplitAt: splitting a coordinate preserves the product measure.
• MeasureTheory.Measure.pi_setOf_apply_eq_apply: two coordinates are almost surely distinct when one of the factors has no atoms.

Implementation notes

[UPSTREAM] candidates: the equivalence for Mathlib/MeasureTheory/MeasurableSpace/Embedding.lean, beside MeasurableEquiv.piFinSuccAbove, and the two theorems for Mathlib/MeasureTheory/Constructions/Pi.lean.

def MeasurableEquiv.piSplitAt {ι : Type u_1} [DecidableEq ι] (α : ι → Type u_2) [(i : ι) → MeasurableSpace (α i)] (i : ι) : ((j : ι) → α j) ≃ᵐ α i × ((j : { j : ι // j ≠ i }) → α ↑j)

Measurable version of Equiv.piSplitAt.

Equations

• MeasurableEquiv.piSplitAt α i = { toEquiv := Equiv.piSplitAt i α, measurable_toFun := ⋯, measurable_invFun := ⋯ }

@[simp]

theorem MeasurableEquiv.piSplitAt_symm_apply {ι : Type u_1} [DecidableEq ι] (α : ι → Type u_2) [(i : ι) → MeasurableSpace (α i)] (i : ι) : ⇑(piSplitAt α i).symm = fun (f : α i × ((j : { j : ι // ¬j = i }) → α ↑j)) (j : ι) => if h : j = i then ⋯ ▸ f.1 else f.2 ⟨j, h⟩

@[simp]

theorem MeasurableEquiv.piSplitAt_apply {ι : Type u_1} [DecidableEq ι] (α : ι → Type u_2) [(i : ι) → MeasurableSpace (α i)] (i : ι) : ⇑(piSplitAt α i) = fun (f : (j : ι) → α j) => (f i, fun (j : { j : ι // ¬j = i }) => f ↑j)

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

Splitting one coordinate off a finite product measure is measure preserving: under Measure.pi μ the i-th coordinate is independent of the others. General-index sibling of measurePreserving_piFinSuccAbove.

theorem MeasureTheory.volume_preserving_piSplitAt {ι : Type u_1} [DecidableEq ι] [Fintype ι] (α : ι → Type u) [(i : ι) → MeasureSpace (α i)] [∀ (i : ι), SigmaFinite volume] (i : ι) : MeasurePreserving (⇑(MeasurableEquiv.piSplitAt α i)) volume volume

measurePreserving_piSplitAt for volume.

theorem MeasureTheory.Measure.pi_setOf_apply_eq_apply {ι : Type u_2} [Fintype ι] [DecidableEq ι] {X : Type u_3} [MeasurableSpace X] [MeasurableEq X] (μ : ι → Measure X) [∀ (i : ι), SigmaFinite (μ i)] {j k : ι} (hjk : j ≠ k) [NullSingletonClass (μ j)] : (Measure.pi μ) {x : ι → X | x j = x k} = 0

Two coordinates of a product measure are almost surely distinct when one has no atoms.