Last-coordinate splitting of finite product spaces

This file records the measurable equivalence ((i : Fin n) → α i.castSucc) × α (Fin.last n) ≃ᵐ (∀ i, α i) given by Fin.snoc, together with the fact that it preserves finite products of sigma-finite measures.

This is Fin.snocEquiv with the product factors swapped, so that the last coordinate is the Prod.snd factor.

This is a temporary project home. Intended Mathlib placement:

• MeasurableEquiv.piFinSnoc and its simp lemmas → Mathlib.MeasureTheory.MeasurableSpace.Embedding, after piFinSuccAbove
• measurePreserving_piFinSnoc, volume_preserving_piFinSnoc → Mathlib.MeasureTheory.Constructions.Pi, after volume_preserving_piFinSuccAbove

TODO: if those lemmas land in Mathlib, delete this file and switch uses to the upstream names.

def MeasurableEquiv.piFinSnoc {n : ℕ} (α : Fin (n + 1) → Type u_1) [(i : Fin (n + 1)) → MeasurableSpace (α i)] : ((i : Fin n) → α i.castSucc) × α (Fin.last n) ≃ᵐ ((i : Fin (n + 1)) → α i)

Measurable equivalence ((i : Fin n) → α i.castSucc) × α (Fin.last n) ≃ᵐ (∀ i, α i) given by Fin.snoc.

Measurable version of Fin.snocEquiv with the product factors swapped.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MeasurableEquiv.piFinSnoc_apply {n : ℕ} (α : Fin (n + 1) → Type u_1) [(i : Fin (n + 1)) → MeasurableSpace (α i)] (p : ((i : Fin n) → α i.castSucc) × α (Fin.last n)) : (piFinSnoc α) p = Fin.snoc p.1 p.2

@[simp]

theorem MeasurableEquiv.piFinSnoc_symm_apply {n : ℕ} (α : Fin (n + 1) → Type u_1) [(i : Fin (n + 1)) → MeasurableSpace (α i)] (f : (i : Fin (n + 1)) → α i) : (piFinSnoc α).symm f = (Fin.init f, f (Fin.last n))

theorem MeasureTheory.measurePreserving_piFinSnoc {n : ℕ} {α : Fin (n + 1) → Type u_1} {m : (i : Fin (n + 1)) → MeasurableSpace (α i)} (μ : (i : Fin (n + 1)) → Measure (α i)) [∀ (i : Fin (n + 1)), SigmaFinite (μ i)] : MeasurePreserving (⇑(MeasurableEquiv.piFinSnoc α)) ((Measure.pi fun (j : Fin n) => μ j.castSucc).prod (μ (Fin.last n))) (Measure.pi μ)

Last-coordinate splitting preserves a finite product of sigma-finite measures.

theorem MeasureTheory.volume_preserving_piFinSnoc {n : ℕ} (α : Fin (n + 1) → Type u_1) [(i : Fin (n + 1)) → MeasureSpace (α i)] [∀ (i : Fin (n + 1)), SigmaFinite volume] : MeasurePreserving (⇑(MeasurableEquiv.piFinSnoc α)) volume volume

Last-coordinate splitting preserves product volume.