expect_dite_eq — Mathlib

English

Fix i ∈ ι and let f : ∀ j, j = i → M. Then the average over j of the dependent if j = i then f j h else 0 equals f(i) divided by card ι.

Русский

Фиксируем i ∈ ι и пусть f : ∀ j, j = i → M. Тогда среднее по j от зависимого ветвления if j = i тогда f(j,h) иначе 0 равно f(i) / card ι.

LaTeX

$$$\mathbb{E}_j (\text{if } j = i \text{ then } f(j, h) \text{ else } 0) = \dfrac{f(i, rfl)}{\\mathrm{card}(\\iota)}$$$

Lean4

theorem expect_dite_eq (i : ι) (f : ∀ j, i = j → M) : 𝔼 j, (if h : i = j then f j h else 0) = f i rfl /ℚ card ι := by
  simp

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