balance_apply

Mathlib.Algebra.BigOperators.Balance

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

English

For any f, balance(f)(x) equals f(x) minus the average of f over the index set.

Русский

Для любой функции f, (balance f)(x) равняется f(x) минус среднее значение f по индексу.

LaTeX

$$balance(f)(x) = f(x) - \\mathbb{E}[f]$$

Lean4

theorem balance_apply (f : ι → G) (x : ι) : balance f x = f x - 𝔼 y, f y :=
  rfl

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

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

Разделы

Аффилиация

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