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