filter — Mathlib

English

Given a PMF p, a set s, and a witness h that ∃ a ∈ s, a ∈ p.support, the filtered PMF p.filter s h is defined as the normalization of the indicator of p on s.

Русский

Для распределения PMF p, множества s и доказательства h того, что ∃ a ∈ s с a ∈ поддержке p, задаётся фильтрованное распределение p.filter s h как нормализация ограниченного на s распределения.

LaTeX

$$$ p.filter\ s\ h = \operatorname{normalize}(s.\operatorname{indicator}(p)) $$$

Lean4

/-- Create new `PMF` by filtering on a set with non-zero measure and normalizing. -/
def filter (p : PMF α) (s : Set α) (h : ∃ a ∈ s, a ∈ p.support) : PMF α :=
  PMF.normalize (s.indicator p) (by simpa using h) (p.tsum_coe_indicator_ne_top s)

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