expect_balance

Mathlib.Algebra.BigOperators.Balance

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

English

Let f be as above. The average of balance f over ι is 0.

Русский

Пусть f как выше. Среднее по балансу balance f на ι равно 0.

LaTeX

$$$$ \\frac{1}{|\\iota|} \\sum_{x \\in \\mathrm{univ}} \\mathrm{balance}(f)(x) = 0. $$$$

Lean4

@[simp]
theorem expect_balance (f : ι → G) : 𝔼 x, balance f x = 0 := by simp [expect]

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

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

Разделы

Аффилиация

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