expect_div — Mathlib

English

Let s be a finite set and f: ι → M. For any a ∈ M, the average of f over s, divided by a, equals the average of f(i)/a over i in s:

Русский

Пусть s — конечное множество и f: ι → M. Для любого a ∈ M выполняется равенство: среднее по s от f(i) делённое на a равно среднему по i∈s от f(i)/a.

LaTeX

$$$\dfrac{\mathbb{E}_{i \\in s} f(i)}{a} = \mathbb{E}_{i \\in s} \dfrac{f(i)}{a}$$$

Lean4

theorem expect_div (s : Finset ι) (f : ι → M) (a : M) : (𝔼 i ∈ s, f i) / a = 𝔼 i ∈ s, f i / a := by
  simp_rw [div_eq_mul_inv, expect_mul]

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