card_smul_expect — Mathlib

English

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

Русский

Для конечного типа ι сумма значений делится на количество элементов; произведение card(ι) на среднее по ι равно сумме по всем i.

LaTeX

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

Lean4

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

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