le_expect — Mathlib

English

If the finite nonempty s has every f(i) ≤ a, then the average is ≤ a.

Русский

Если у конечного непустого набора s для всех i выполняется f(i) ≤ a, то среднее по s ≤ a.

LaTeX

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

Lean4

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

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