balance — Mathlib

English

The balancing of a function f is defined as the function f minus its average value over the finite index type.

Русский

Балансировка функции f определяется как сама функция минус её среднее значение по конечному индексу.

LaTeX

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

Lean4

/-- The balancing of a function, namely the function minus its average. -/
def balance (f : ι → G) : ι → G :=
  f - Function.const _ (𝔼 y, f y)

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