expect — Mathlib

English

The average of a function over a finite set s is the sum over i∈s of f(i) divided by the cardinality of s.

Русский

Среднее значения функции по конечному множеству s равно сумме значений функции на i∈s, делённой на кардинал множества s.

LaTeX

$$$$ \\mathbb{E}_{i \\in s} f(i) = \\frac{1}{|s|} \\sum_{i \\in s} f(i). $$$$

Lean4

/-- Average of a function over a finset. If the finset is empty, this is equal to zero. -/
def expect [AddCommMonoid M] [Module ℚ≥0 M] (s : Finset ι) (f : ι → M) : M :=
  (#s : ℚ≥0)⁻¹ • ∑ i ∈ s, f i

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