English
If a is fixed and f defines PMF β for every a in the support of the pure distribution at a, then (pure a).bindOnSupport f equals f(a, proof).
Русский
Если фиксировано a, и для каждого a в опоре чистого распределения определено PMF β через f, то (pure a).bindOnSupport f = f(a, доказательство).
LaTeX
$$$$ (\\mathrm{pure}(a)).\\bindOnSupport f = f(a, (\\mathrm{mem\\_support\\_pure\\_iff}\ \ a\ a)^{-1} \\text{(mpr } rfl)) $$$$
Lean4
@[simp]
theorem pure_bindOnSupport (a : α) (f : ∀ (a' : α) (_ : a' ∈ (pure a).support), PMF β) :
(pure a).bindOnSupport f = f a ((mem_support_pure_iff a a).mpr rfl) :=
by
refine PMF.ext fun b => ?_
simp only [bindOnSupport_apply, pure_apply]
classical
refine _root_.trans (tsum_congr fun a' => ?_) (tsum_ite_eq a _)
by_cases h : a' = a <;> simp [h]
