English
Binding using bindOnSupport twice distributes: (p.bindOnSupport f).bindOnSupport g equals p.bindOnSupport (λ a ha, (f a ha).bindOnSupport (λ b hb, g b (mem_support_bindOnSupport_iff f b).mpr ⟨a, ha, hb⟩)).
Русский
Повторное применение bindOnSupport распадается на единообразное выражение: (p.bindOnSupport f).bindOnSupport g = p.bindOnSupport (λ a ha, (f a ha).bindOnSupport (λ b hb, g b (¬∃)).
LaTeX
$$$$ (\\mathrm{bindOnSupport}(p, f)).\\mathrm{bindOnSupport}(g) = \\mathrm{bindOnSupport}\\left(p, \\lambda a ha. (f(a, ha)).\\mathrm{bindOnSupport}(\\lambda b hb. g(b, hb) )\\right) $$$$
Lean4
@[simp]
theorem bindOnSupport_bindOnSupport (p : PMF α) (f : ∀ a ∈ p.support, PMF β)
(g : ∀ b ∈ (p.bindOnSupport f).support, PMF γ) :
(p.bindOnSupport f).bindOnSupport g =
p.bindOnSupport fun a ha =>
(f a ha).bindOnSupport fun b hb => g b ((mem_support_bindOnSupport_iff f b).mpr ⟨a, ha, hb⟩) :=
by
refine PMF.ext fun a => ?_
dsimp only [bindOnSupport_apply]
simp only [← tsum_dite_right, ENNReal.tsum_mul_left.symm, ENNReal.tsum_mul_right.symm]
classical
simp only [ENNReal.tsum_eq_zero]
refine ENNReal.tsum_comm.trans (tsum_congr fun a' => tsum_congr fun b => ?_)
split_ifs with h _ h_1 H h_2
any_goals ring1
· absurd H
simpa [h] using h_1 a'
· simp [h_2]
