English
If m is subadditive and respects rational scaling, then for any finite nonempty s and f, m of the average is bounded by the average of m(f(i)).
Русский
Если m субаддитивна и сохраняет рациональные деления, то для непустого конечного s верно неравенство над средними значениями.
LaTeX
$$$s.Nonempty \\Rightarrow m(\\mathbb{E}_{i\\in s} f(i)) \\le \\mathbb{E}_{i\\in s} m(f(i))$$$
Lean4
/-- If `m : M → N` is a subadditive function (`m (a + b) ≤ m a + m b`) and `s` is a nonempty set,
then `m (𝔼 i ∈ s, f i) ≤ 𝔼 i ∈ s, m (f i)`. -/
theorem le_expect_nonempty_of_subadditive (m : M → N) (h_mul : ∀ a b, m (a + b) ≤ m a + m b)
(h_div : ∀ (n : ℕ) a, m (a /ℚ n) = m a /ℚ n) (hs : s.Nonempty) : m (𝔼 i ∈ s, f i) ≤ 𝔼 i ∈ s, m (f i) :=
le_expect_nonempty_of_subadditive_on_pred (p := fun _ ↦ True) (by simpa) (by simp) (by simpa) hs (by simp)
