expect_mul_expect — Mathlib

English

Let f: ι → M and g: κ → M with M a semiring and suitable scalar tower. Then the product of the averages equals the double average of products:

Русский

Пусть f: ι → M и g: κ → M, тогда произведение средних равно двойному среднему по произведениям.

LaTeX

$$$\left(\mathbb{E}_{i} f(i)\right) \cdot \mathbb{E}_{j} g(j) = \mathbb{E}_{i} \mathbb{E}_{j} \big( f(i) \cdot g(j) \big)$$$

Lean4

theorem expect_mul_expect [IsScalarTower ℚ≥0 M M] [SMulCommClass ℚ≥0 M M] (f : ι → M) (g : κ → M) :
    (𝔼 i, f i) * 𝔼 j, g j = 𝔼 i, 𝔼 j, f i * g j :=
  Finset.expect_mul_expect ..

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