abs_expect_le — Mathlib

English

For any finite s and any function f, the absolute value of the average is bounded by the average of absolute values: |\mathbb{E}_{i∈s} f(i)| ≤ \mathbb{E}_{i∈s} |f(i)|.

Русский

Абсолютное значение среднего не превосходит среднего абсолютных значений.

LaTeX

$$$|\\mathbb{E}_{i∈s} f(i)| ≤ \\mathbb{E}_{i∈s} |f(i)|$$$

Lean4

theorem abs_expect_le (s : Finset ι) (f : ι → α) : |𝔼 i ∈ s, f i| ≤ 𝔼 i ∈ s, |f i| :=
  le_expect_of_subadditive abs_zero abs_add_le (fun _ ↦ abs_nnqsmul _)

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