expect_ite_mem — Mathlib

English

Let s and f be as above; the average of ite(i∈t, f(i), 0) equals (#(s∩t)/#s) times the average over s∩t of f.

Русский

Пусть s, t и функции f, определения аналогичны; среднее ite(i∈t, f(i), 0) по i∈s равно ((|s∩t|)/|s|) умножить на среднее по s∩t функции f.

LaTeX

$$$$ \\mathbb{E}_{i \\in s} \\mathrm{ite}(i \\in t, f(i), 0) = \\frac{|s \\cap t|}{|s|} \\mathbb{E}_{i \\in s \\cap t} f(i). $$$$

Lean4

theorem expect_ite_mem (s t : Finset ι) (f : ι → M) :
    𝔼 i ∈ s, (if i ∈ t then f i else 0) = (#(s ∩ t) / #s : ℚ≥0) • 𝔼 i ∈ s ∩ t, f i :=
  by
  obtain hst | hst := (s ∩ t).eq_empty_or_nonempty
  · simp [expect, hst]
  · simp [expect, smul_smul, ← inv_mul_eq_div, hst.card_ne_zero]

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