English
Let p be a probability mass function on α and q be a probability mass function on β. If we bind p with a constant β-distribution q, we obtain q itself. In other words, sampling from p and then always sampling from q yields the same distribution as sampling directly from q.
Русский
Пусть p — распределение массы на α, q — распределение массы на β. Связывание p константным распределением q возвращает q самo по себе. Иначе говоря, выбор из p, после чего всегда выбор из q, дает то же распределение, что и выбор из q.
LaTeX
$$$$ \\mathrm{bind}(p, \\lambda x. q) = q $$$$
Lean4
@[simp]
theorem bind_const (p : PMF α) (q : PMF β) : (p.bind fun _ => q) = q :=
PMF.ext fun x => by rw [bind_apply, ENNReal.tsum_mul_right, tsum_coe, one_mul]
