English
Generalizes bind by allowing f to be defined only on the support of p. The resulting PMF on β is given by (p.bindOnSupport f)(b) = ∑' a p(a) if a ∈ supp(p) then f(a, ha)(b) else 0.
Русский
Обобщение операции связывания: f определен только на опоре p. Результирующее PMF β задается как (p.bindOnSupport f)(b) = ∑' a p(a) ⋅ f(a, ha)(b), где ha — доказательство принадлежности a опоре p (нужный член суммирования берется только при a ∈ supp(p)).
LaTeX
$$$$ (p.bindOnSupport f)(b) = \\sum' a \\, p(a) \\cdot \\begin{cases} f(a, h)(b), & \\text{if } h : a \\in \\mathrm{supp}(p), \\\\ 0, & \\text{otherwise} \\end{cases} $$$$
Lean4
/-- Generalized version of `bind` allowing `f` to only be defined on the support of `p`.
`p.bind f` is equivalent to `p.bindOnSupport (fun a _ ↦ f a)`, see `bindOnSupport_eq_bind`. -/
def bindOnSupport (p : PMF α) (f : ∀ a ∈ p.support, PMF β) : PMF β :=
⟨fun b => ∑' a, p a * if h : p a = 0 then 0 else f a h b,
ENNReal.summable.hasSum_iff.2
(by
refine ENNReal.tsum_comm.trans (_root_.trans (tsum_congr fun a => ?_) p.tsum_coe)
simp_rw [ENNReal.tsum_mul_left]
split_ifs with h
· simp only [h, zero_mul]
· rw [(f a h).tsum_coe, mul_one])⟩
