card_mul_expect — Mathlib

English

For a finite set s, the sum of f over s equals the cardinality times the average: ∑_{i∈s} f(i) = |s| · E_{i∈s} f(i).

Русский

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

LaTeX

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

Lean4

@[simp]
theorem card_mul_expect (s : Finset ι) (f : ι → M) : #s * 𝔼 i ∈ s, f i = ∑ i ∈ s, f i := by
  rw [← nsmul_eq_mul, card_smul_expect]

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