English
Let p be a PMF on α, f a family of PMFs on β depending on α, and g a family of PMFs on γ depending on β. Then binding p with f and then with g is the same as binding p with the function a ↦ (f(a)) bound by g. This is the associativity of the bind operation for PMFs.
Русский
Пусть p — PMF на α, f — семействo PMF β зависящих от α, и g — семействo PMF γ зависящих от β. Тогда последовательное связывание p с f и далее с g равно связыванию p с функцией a ↦ (f(a)) ⋯ g. Это ассоциативность операции связывания PMF.
LaTeX
$$$$ (\\mathrm{bind}(\\mathrm{bind}(p, f), g) = \\mathrm{bind}\\left(p, \\lambda a. \\mathrm{bind}(f(a), g)\\right) \\right) $$$$
Lean4
@[simp]
theorem bind_bind : (p.bind f).bind g = p.bind fun a => (f a).bind g :=
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
