expect_le_expect — Mathlib

English

A beta-reduced monotone version of the expect-inequality: if f ≤ g componentwise, then the Finset expect of f is ≤ that of g.

Русский

Упрощённая монотонная версия неравенства ожиданий: если f i ≤ g i для каждого i∈s, то s.expect f ≤ s.expect g.

LaTeX

$$$\\text{If } \\forall i\\in s, f(i) \\le g(i),\\; s\\text{.expect } f \\le s\\text{.expect } g$$$

Lean4

theorem expect_le_expect (hfg : ∀ i ∈ s, f i ≤ g i) : 𝔼 i ∈ s, f i ≤ 𝔼 i ∈ s, g i :=
  smul_le_smul_of_nonneg_left (sum_le_sum hfg) <| by positivity

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