card_mul_expect — Mathlib

English

For a finite type ι, the sum over all indices equals the card(ι) times the average: ∑_{i} f(i) = |ι| · E_{i∈ι} f(i).

Русский

Для конечного типа ι сумма по всем индексам равна cardinality типа, умноженной на среднее: ∑_{i} f(i) = |ι| · E_{i∈ι} f(i).

LaTeX

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

Lean4

@[simp]
theorem _root_.Fintype.card_mul_expect [Fintype ι] (f : ι → M) : Fintype.card ι * 𝔼 i, f i = ∑ i, f i :=
  Finset.card_mul_expect _ _

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