English
There is a measure-preserving equivalence between the sum-pi construction and the product of pi-projections across respective index sets.
Русский
Существует мера-производящая эквивалентность между конструкцией sumPi и произведением pi-проекций по соответствующим наборам индексов.
LaTeX
$$measurePreserving_sumPiEquivProdPi (X) :$$
Lean4
theorem measurePreserving_sumPiEquivProdPi_symm {X : ι ⊕ ι' → Type*} {m : ∀ i, MeasurableSpace (X i)}
(μ : ∀ i, Measure (X i)) [∀ i, SigmaFinite (μ i)] :
MeasurePreserving (MeasurableEquiv.sumPiEquivProdPi X).symm
((Measure.pi fun i => μ (.inl i)).prod (Measure.pi fun i => μ (.inr i))) (Measure.pi μ)
where
measurable := (MeasurableEquiv.sumPiEquivProdPi X).symm.measurable
map_eq := by
refine (pi_eq fun s _ => ?_).symm
simp_rw [MeasurableEquiv.map_apply, MeasurableEquiv.coe_sumPiEquivProdPi_symm,
Equiv.sumPiEquivProdPi_symm_preimage_univ_pi, Measure.prod_prod, Measure.pi_pi, Fintype.prod_sum_type]
