smul_expect — Mathlib

English

Let a be a scalar acting on M and s ⊆ ι finite. Then a · E_{i∈s} f(i) = E_{i∈s} a · f(i).

Русский

Пусть a является скаляром в M. Тогда a умножить на среднее по s от f равно среднему по s от a·f.

LaTeX

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

Lean4

theorem smul_expect {G : Type*} [DistribSMul G M] [SMulCommClass G ℚ≥0 M] (a : G) (s : Finset ι) (f : ι → M) :
    a • 𝔼 i ∈ s, f i = 𝔼 i ∈ s, a • f i := by simp only [expect, smul_sum, smul_comm]

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