expect_eq_sum_div_card — Mathlib

English

For any finite set s and function f, the average equals the sum divided by the cardinality: E_{i∈s} f(i) = (∑_{i∈s} f(i)) / |s|.

Русский

Для любого конечного множества s и функции f среднее равно сумме деленной на кардинал: E_{i∈s} f(i) = (∑_{i∈s} f(i)) / |s|.

LaTeX

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

Lean4

theorem expect_eq_sum_div_card (s : Finset ι) (f : ι → M) : 𝔼 i ∈ s, f i = (∑ i ∈ s, f i) / #s := by
  rw [expect, NNRat.smul_def, div_eq_inv_mul, NNRat.cast_inv, NNRat.cast_natCast]

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