expect_dite_eq — Mathlib

English

For i, a dependent f on i with f(j,i) mapping, the average of if h: j=i then f(j,h) else 0 equals f(i,i)/|s| if i∈s, else 0.

Русский

Для зависимого от i f(j,i) среднего значения if h: j=i then f(j,h) else 0 равняется f(i,rfl)/|s| при i∈s и 0 иначе.

LaTeX

$$$$ \\mathbb{E}_{j \\in s} \\left( \\begin{cases} f(j,h) & \\text{if } h: j=i \\\\ 0 & \\text{otherwise} \\end{cases} \\right) = \\begin{cases} \\dfrac{f(i, rfl)}{|s|}, & i \\in s \\\\ 0, & i \\notin s \\end{cases}. $$$$

Lean4

@[simp]
theorem expect_dite_eq (i : ι) (f : ∀ j, i = j → M) :
    𝔼 j ∈ s, (if h : i = j then f j h else 0) = if i ∈ s then f i rfl /ℚ #s else 0 := by split_ifs <;> simp [expect, *]

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