filter_apply — Mathlib

English

For any a, the value of the filtered PMF at a equals the product of the indicator that a ∈ s with the inverse of the total mass on s inside p.

Русский

Значение фильтрованной массы в точке a равно произведению индикатора того, что a ∈ s, и обратной сумме массы по s внутри p.

LaTeX

$$$ (p.filter\ s\ h)(a) = (s.\operatorname{indicator}(p))(a) \cdot \Big(\sum_{a'} (s.\operatorname{indicator}(p))(a')\Big)^{-1} $$$

Lean4

@[simp]
theorem filter_apply (a : α) : (p.filter s h) a = s.indicator p a * (∑' a', (s.indicator p) a')⁻¹ := by
  rw [filter, normalize_apply]

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