expect_eq_sum_div_card — Mathlib

English

Let I be a finite index set and f: I → M, where M is a semifield of characteristic zero. Then the average value of f over I equals the sum of f(i) divided by the cardinality of I: ∑_{i∈I} f(i) / |I| = average of f over I.

Русский

Пусть I — конечное множество индексов и функция f: I → M, где M — полуполе нулевой характеристики. Тогда среднее значение f по I равно сумме значений f(i) по i делённой на карточность I:

LaTeX

$$$\\mathbb{E}_{i \\in \\iota} f(i) = \dfrac{\\sum_{i \\in \\iota} f(i)}{\\lvert \\iota \\rvert}$$$

Lean4

theorem _root_.Fintype.expect_eq_sum_div_card [Fintype ι] (f : ι → M) : 𝔼 i, f i = (∑ i, f i) / Fintype.card ι :=
  Finset.expect_eq_sum_div_card _ _

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