expect_le — Mathlib

English

If s is nonempty and every f(i) is nonnegative on s, then averaging preserves nonnegativity: the expectation is nonnegative.

Русский

Если s непусто и все f(i) ≥ 0 для i∈s, то среднее по s неотрицательно.

LaTeX

$$$s\\neq \\varnothing \\Rightarrow (\\forall i\\in s, f(i) \\ge 0) \\Rightarrow 0 \\le s\\!\\text{expect } f$$$

Lean4

theorem expect_le (hs : s.Nonempty) (h : ∀ x ∈ s, f x ≤ a) : 𝔼 i ∈ s, f i ≤ a :=
  (inv_smul_le_iff_of_pos <| mod_cast hs.card_pos).2 <| by rw [Nat.cast_smul_eq_nsmul]; exact sum_le_card_nsmul _ _ _ h

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