expect_mul — Mathlib

English

Let S be a finite index set and f : S → M. Then for a scalar a, a · E_{i∈S} f(i) = E_{i∈S} a · f(i).

Русский

Пусть S — конечный индексный набор, f:S→M. Тогда для скаляра a: a · E_{i∈S} f(i) = E_{i∈S} a · f(i).

LaTeX

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

Lean4

theorem expect_mul [IsScalarTower ℚ≥0 M M] (s : Finset ι) (f : ι → M) (a : M) : (𝔼 i ∈ s, f i) * a = 𝔼 i ∈ s, f i * a :=
  by rw [expect, expect, smul_mul_assoc, sum_mul]

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