English
A certain natural bijection between a pi-product space and a product of restricted pi-spaces preserves measure.
Русский
Естественное биекция между пространством произведения по пи и произведением ограниченных пи-пространств сохраняет меру.
LaTeX
$$$MeasurePreserving(\mathrm{piEquivPiSubtypeProd}(\alpha,p))\; (Measure.pi(\mu))\; ((\mathrm{pi} i : Subtype(p) => \mu i) .prod (\mathrm{pi} i => \mu i))$$$
Lean4
theorem measurePreserving_piEquivPiSubtypeProd (p : ι → Prop) [DecidablePred p] :
MeasurePreserving (MeasurableEquiv.piEquivPiSubtypeProd α p) (Measure.pi μ)
((Measure.pi fun i : Subtype p => μ i).prod (Measure.pi fun i => μ i)) :=
by
set e := (MeasurableEquiv.piEquivPiSubtypeProd α p).symm
refine MeasurePreserving.symm e ?_
refine ⟨e.measurable, (pi_eq fun s _ => ?_).symm⟩
have : e ⁻¹' pi univ s = (pi univ fun i : { i // p i } => s i) ×ˢ pi univ fun i : { i // ¬p i } => s i :=
Equiv.preimage_piEquivPiSubtypeProd_symm_pi p s
rw [e.map_apply, this, prod_prod, pi_pi, pi_pi]
exact Fintype.prod_subtype_mul_prod_subtype p fun i => μ i (s i)
