English
If f does not depend on the additional hypothesis and is simply a function a ↦ PMF β, then binding on the support coincides with the ordinary bind: (p.bindOnSupport (λ a, f a)) = p.bind f.
Русский
Если функция f по смыслу не зависит от дополнительного гипотеза и есть обычная функция a ↦ PMF β, то связывание по опоре совпадает с обычным связыванием: (p.bindOnSupport (λ a, f a)) = p.bind f.
LaTeX
$$$$ (p.bindOnSupport (\\lambda a. f(a))) = p.bind f $$$$
Lean4
/-- `bindOnSupport` reduces to `bind` if `f` doesn't depend on the additional hypothesis. -/
@[simp]
theorem bindOnSupport_eq_bind (p : PMF α) (f : α → PMF β) : (p.bindOnSupport fun a _ => f a) = p.bind f :=
by
ext b
have : ∀ a, ite (p a = 0) 0 (p a * f a b) = p a * f a b := fun a =>
ite_eq_right_iff.2 fun h => h.symm ▸ symm (zero_mul <| f a b)
simp only [bindOnSupport_apply fun a _ => f a, p.bind_apply f, dite_eq_ite, mul_ite, mul_zero, this]
