English
Changing the order of two bindOnSupport operations yields the same result: (p.bindOnSupport (λ a ha, q.bindOnSupport (f a ha))) equals q.bindOnSupport (λ b hb, p.bindOnSupport (λ a ha, f a ha b) ).
Русский
Изменение порядка двух операций bindOnSupport дает тот же результат: (p.bindOnSupport (λ a ha, q.bindOnSupport (f a ha))) эквивалентно q.bindOnSupport (λ b hb, p.bindOnSupport (λ a ha, f a ha b))).
LaTeX
$$$$ (p.bindOnSupport (\\lambda a ha. q.bindOnSupport (f a ha))) = q.bindOnSupport (\\lambda b hb. p.bindOnSupport (\\lambda a ha. f a ha b)) $$$$
Lean4
theorem bindOnSupport_comm (p : PMF α) (q : PMF β) (f : ∀ a ∈ p.support, ∀ b ∈ q.support, PMF γ) :
(p.bindOnSupport fun a ha => q.bindOnSupport (f a ha)) =
q.bindOnSupport fun b hb => p.bindOnSupport fun a ha => f a ha b hb :=
by
apply PMF.ext; rintro c
simp only [bindOnSupport_apply, ← tsum_dite_right, ENNReal.tsum_mul_left.symm]
refine _root_.trans ENNReal.tsum_comm (tsum_congr fun b => tsum_congr fun a => ?_)
split_ifs with h1 h2 h2 <;> ring
