bindOnSupport_apply — Mathlib

English

For any b in β, (p.bindOnSupport f) b equals the sum ∑' a p(a) times f(a, ha) b, i.e., the pointwise value is given by summing over the support with the appropriate conditional PMFs.

Русский

Для любого b ∈ β значение (p.bindOnSupport f) b равно сумме ∑' a p(a) ⋅ f(a, ha) b, т.е. значение в точке даётся суммированием по опоре с соответствующими условными PMF.

LaTeX

$$$$ (p.bindOnSupport f)(b) = \\sum' a \\, p(a) \\cdot \\begin{cases} f(a,h)(b), & h: a \\in \\mathrm{supp}(p), \\\\ 0, & \\text{иначе} \\end{cases} $$$$

Lean4

@[simp]
theorem bindOnSupport_apply (b : β) : p.bindOnSupport f b = ∑' a, p a * if h : p a = 0 then 0 else f a h b :=
  rfl

Похожие утверждения