expect_neg_distrib — Mathlib

English

The average of a difference equals the difference of averages: E_{i∈s} (f(i) − g(i)) = E_{i∈s} f(i) − E_{i∈s} g(i).

Русский

Среднее разности равно разности средних: E_{i∈s} (f(i) − g(i)) = E_{i∈s} f(i) − E_{i∈s} g(i).

LaTeX

$$$\mathbb{E}_{i\in s} (f(i) - g(i)) = \mathbb{E}_{i\in s} f(i) - \mathbb{E}_{i\in s} g(i).$$$

Lean4

@[simp]
theorem expect_neg_distrib (s : Finset ι) (f : ι → M) : 𝔼 i ∈ s, -f i = -𝔼 i ∈ s, f i := by simp [expect]

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