English
The product of a dirac measure with another measure equals the pushforward by the pairing map: dirac x × ν equals map (λ z. (z, x)) ν.
Русский
Произведение шара директивной меры на другую меру равно отображению по затем вычисляемому отображению: dirac x ⨂ ν = map (λ z. (z, x)) ν.
LaTeX
$$$(\\mathrm{dirac}\\,x) \\prod ν = \\mathrm{map}(\\lambda z. (z,x))\, ν$$$
Lean4
theorem prodAssoc_prod [SFinite τ] : map MeasurableEquiv.prodAssoc ((μ.prod ν).prod τ) = μ.prod (ν.prod τ) :=
by
have :
sum (fun (p : ℕ × ℕ × ℕ) ↦ (sfiniteSeq μ p.1).prod ((sfiniteSeq ν p.2.1).prod (sfiniteSeq τ p.2.2))) =
sum (fun (p : (ℕ × ℕ) × ℕ) ↦ (sfiniteSeq μ p.1.1).prod ((sfiniteSeq ν p.1.2).prod (sfiniteSeq τ p.2))) :=
by
ext s hs
rw [sum_apply _ hs, sum_apply _ hs, ← (Equiv.prodAssoc _ _ _).tsum_eq]
simp only [Equiv.prodAssoc_apply]
rw [← sum_sfiniteSeq μ, ← sum_sfiniteSeq ν, ← sum_sfiniteSeq τ, prod_sum, prod_sum,
map_sum MeasurableEquiv.prodAssoc.measurable.aemeasurable, prod_sum, prod_sum, this]
congr
ext1 i
refine
(prod_eq_generateFrom generateFrom_measurableSet generateFrom_prod isPiSystem_measurableSet isPiSystem_prod
((sfiniteSeq μ i.1.1)).toFiniteSpanningSetsIn
((sfiniteSeq ν i.1.2).toFiniteSpanningSetsIn.prod (sfiniteSeq τ i.2).toFiniteSpanningSetsIn) ?_).symm
rintro s hs _ ⟨t, ht, u, hu, rfl⟩; rw [mem_setOf_eq] at hs ht hu
simp_rw [map_apply (MeasurableEquiv.measurable _) (hs.prod (ht.prod hu)), MeasurableEquiv.prodAssoc,
MeasurableEquiv.coe_mk, Equiv.prod_assoc_preimage, prod_prod, mul_assoc]
