English
If a subadditive function m is compatible with division by rationals, then the inequality for expectations remains valid in the limit regime; i.e., as you refine the index set, the bound persists.
Русский
При субаддитивности и совместимости с делением на рациональные сохраняется неравенство для ожидания в пределе.
LaTeX
$$$\\text{le_expect_nonempty_of_subadditive_on_pred}$$$
Lean4
/-- If `m` is a subadditive function (`m (x + y) ≤ m x + m y`, `m 0 = 0`) preserved under division
by a natural, then `m (𝔼 i ∈ s, f i) ≤ 𝔼 i ∈ s, m (f i)`. -/
theorem le_expect_of_subadditive (h_zero : m 0 = 0) (h_add : ∀ a b, m (a + b) ≤ m a + m b)
(h_div : ∀ (n : ℕ) a, m (a /ℚ n) = m a /ℚ n) : m (𝔼 i ∈ s, f i) ≤ 𝔼 i ∈ s, m (f i) :=
le_expect_of_subadditive_on_pred (p := fun _ ↦ True) h_zero (by simpa) (by simp) (by simpa) (by simp)
