expect_ite_zero — Mathlib

English

For a finite s and predicate p, the average of ite(p(i), a, 0) equals a/|s| if ∃ i∈s, p(i), otherwise 0.

Русский

Для конечного s и предиката p среднее значения ite(p(i), a, 0) равно a/|s|, если существует i∈s, такое что p(i); иначе 0.

LaTeX

$$$$ \\mathbb{E}_{i \\in s} \\mathrm{ite}(p(i), a, 0) = \\begin{cases} \\dfrac{a}{|s|}, & \\exists i \\in s, p(i) \\\\ 0, & \\text{иначе} \\end{cases}. $$$$

Lean4

theorem expect_ite_zero (s : Finset ι) (p : ι → Prop) [DecidablePred p] (h : ∀ i ∈ s, ∀ j ∈ s, p i → p j → i = j)
    (a : M) : 𝔼 i ∈ s, ite (p i) a 0 = ite (∃ i ∈ s, p i) (a /ℚ #s) 0 := by
  split_ifs <;> simp [expect, sum_ite_zero _ _ h, *]

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