expect_ite_eq

Mathlib.Algebra.BigOperators.Expect

URI: https://scilib.ai/kg/mathlib#Fintype.expect_ite_eq

English

For a fixed i, the average over j of the indicator that j = i times f j equals f i divided by card ι.

Русский

Для фиксированного i среднее по j от (if j = i then f(j) else 0) равно f(i) / card ι.

LaTeX

$$$\mathbb{E}_j (\mathbf{1}_{j=i} f(j)) = \dfrac{f(i)}{\\mathrm{card}(\\iota)}$$$

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru