English
If m is subadditive with p preserved, then for nonempty s, and f taking values in the predicate p, m of the s-average is ≤ the average of m(f(i)).
Русский
Если m субаддитивна и сохраняет pred-предикат, то для непустого s и f, взятого в pred, выполняется неравенство над средними.
LaTeX
$$$s.Nonempty → (∀ i∈s, p(f(i))) → m(\\mathbb{E}_{i∈s} f(i)) ≤ \\mathbb{E}_{i∈s} m(f(i))$$$
Lean4
/-- Let `{a | p a}` be a subsemigroup of a commutative monoid `M`. If `m` is a subadditive function
(`m (x + y) ≤ m x + m y`, `m 0 = 0`) preserved under division by a natural and `f` is a function
valued in that subsemigroup, then `m (𝔼 i ∈ s, f i) ≤ 𝔼 i ∈ s, m (f i)`. -/
theorem le_expect_of_subadditive_on_pred (h_zero : m 0 = 0) (h_add : ∀ a b, p a → p b → m (a + b) ≤ m a + m b)
(hp_add : ∀ a b, p a → p b → p (a + b)) (h_div : ∀ (n : ℕ) a, p a → m (a /ℚ n) = m a /ℚ n) (hs : ∀ i ∈ s, p (f i)) :
m (𝔼 i ∈ s, f i) ≤ 𝔼 i ∈ s, m (f i) :=
by
obtain rfl | hs_nonempty := s.eq_empty_or_nonempty
· simp [h_zero]
· exact le_expect_nonempty_of_subadditive_on_pred h_add hp_add h_div hs_nonempty hs
