English
For two finite index sets s and t that are disjoint, the piFinsetUnion map is measure-preserving between the product measure over s and t and the pi-measure over their union.
Русский
При двух непересекающихся конечных множествах индексов s и t отображение piFinsetUnion сохраняет меру между произведением по s и t и мерой над их объединением.
LaTeX
$$$ \mathrm{MeasurePreserving}\bigl(\mathrm{MeasurableEquiv.piFinsetUnion}(\alpha,h)\bigr)\; (\mathrm{Measure.pi}\mu_i)\; (\mathrm{Measure.pi}\mu_i) $$$
Lean4
theorem measurePreserving_piFinsetUnion {ι : Type*} {α : ι → Type*} {_ : ∀ i, MeasurableSpace (α i)} [DecidableEq ι]
{s t : Finset ι} (h : Disjoint s t) (μ : ∀ i, Measure (α i)) [∀ i, SigmaFinite (μ i)] :
MeasurePreserving (MeasurableEquiv.piFinsetUnion α h)
((Measure.pi fun i : s ↦ μ i).prod (Measure.pi fun i : t ↦ μ i)) (Measure.pi fun i : ↥(s ∪ t) ↦ μ i) :=
let e := Equiv.Finset.union s t h
measurePreserving_piCongrLeft (fun i : ↥(s ∪ t) ↦ μ i) e |>.comp <|
measurePreserving_sumPiEquivProdPi_symm fun b ↦ μ (e b)
