English
Let p be a PMF on α, q a PMF on β, and f a function from α×β to PMF γ. The process of first binding p with f in the α-variable and then binding the result with g is the same as first binding q with a function of b and then binding p with the corresponding function of a. This expresses a commutativity-like property of nested binds.
Русский
Пусть p — PMF на α, q — PMF на β, и f: α×β → PMF γ. Процесс сначала связывания p с f по переменной α, затем связывания результата с g эквивалентен сначала связыванию q с функцией от b, а затем связыванию p с соответствующей функцией от a. Это свойство подобно коммутативности вложенных связок.
LaTeX
$$$$ \\mathrm{bind}(p, \\lambda a. \\mathrm{bind}(q, \\lambda b. f(a,b))) = \\mathrm{bind}(q, \\lambda b. \\mathrm{bind}(p, \\lambda a. f(a,b))) $$$$
Lean4
theorem bind_comm (p : PMF α) (q : PMF β) (f : α → β → PMF γ) :
(p.bind fun a => q.bind (f a)) = q.bind fun b => p.bind fun a => f a b :=
PMF.ext fun b => by
simpa only [ENNReal.coe_inj.symm, bind_apply, ENNReal.tsum_mul_left.symm, ENNReal.tsum_mul_right.symm, mul_assoc,
mul_left_comm, mul_comm] using ENNReal.tsum_comm
