norm_expect_le — Mathlib

English

For any finite index set s and function f: ι → E, the norm of the average is at most the average of norms.

Русский

Для конечного множества индексов s и функции f: ι → E справедливо неравенство нормы среднего: ‖E_{i∈s} f(i)‖ ≤ E_{i∈s} ‖f(i)‖.

LaTeX

$$$$ \\left\\| \\mathbb{E}_{i \\in s} f(i) \\right\\| \\le \\mathbb{E}_{i \\in s} \\| f(i) \\|.$$$$

Lean4

@[bound]
theorem norm_expect_le {ι : Type*} {s : Finset ι} {f : ι → E} : ‖𝔼 i ∈ s, f i‖ ≤ 𝔼 i ∈ s, ‖f i‖ :=
  Finset.le_expect_of_subadditive norm_zero norm_add_le fun _ _ ↦ by rw [norm_nnqsmul K]

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