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]