English
Two finite measures μ and ν on (α × β) × γ are equal iff they agree on all products (s × t) × u with measurable s, t, u.
Русский
Две конечные меры μ и ν на (α × β) × γ равны тогда и только тогда, когда они совпадают на всех множествах вида (s × t) × u с измеримыми s, t, u.
LaTeX
$$$μ = ν \\iff \\forall s,t,u,\\; \\text{MeasurableSet}(s) \\to \\text{MeasurableSet}(t) \\to \\text{MeasurableSet}(u) \\to μ((s ×ˢ t) ×ˢ u) = ν((s ×ˢ t) ×ˢ u)$$$
Lean4
theorem prod_swap : map Prod.swap (μ.prod ν) = ν.prod μ :=
by
have :
sum (fun (i : ℕ × ℕ) ↦ map Prod.swap ((sfiniteSeq μ i.1).prod (sfiniteSeq ν i.2))) =
sum (fun (i : ℕ × ℕ) ↦ map Prod.swap ((sfiniteSeq μ i.2).prod (sfiniteSeq ν i.1))) :=
by
ext s hs
rw [sum_apply _ hs, sum_apply _ hs]
exact ((Equiv.prodComm ℕ ℕ).tsum_eq _).symm
rw [← sum_sfiniteSeq μ, ← sum_sfiniteSeq ν, prod_sum, prod_sum, map_sum measurable_swap.aemeasurable, this]
congr 1
ext1 i
refine (prod_eq ?_).symm
intro s t hs ht
simp_rw [map_apply measurable_swap (hs.prod ht), preimage_swap_prod, prod_prod, mul_comm]
