English
A variant of the dependent-if equality with alternative presentation; the average over s of if h: j=i then f j h else 0 equals the same expression as above with a different form.
Русский
Вариант предыдущего утверждения с иной формой записи; среднее по s от if h: j=i then f j h else 0 равно соответствующему выражению.
LaTeX
$$$$ \\mathbb{E}_{j \\in s} \\left( \\text{if } h : j=i \\text{ then } f(j,h) \\text{ else } 0 \\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, j = i → M) :
𝔼 j ∈ s, (if h : j = i then f j h else 0) = if i ∈ s then f i rfl /ℚ #s else 0 := by split_ifs <;> simp [expect, *]
