English
Let m be a subadditive function between additive monoids, with division by rationals compatible with m; then for any nonempty s, the averaged m(f) dominates m of the average.
Русский
Пусть m — субаддитивная функция между аддитивными моноидами, совместимая с делением на рациональные; тогда для любого непустого s выполняется неравенство над средним.
LaTeX
$$$s\\neq \\varnothing \\Rightarrow m(\\mathbb{E}_{i\\in s} f(i)) \\le \\mathbb{E}_{i\\in s} m(f(i))$$$
Lean4
/-- Let `{a | p a}` be an additive subsemigroup of an additive commutative monoid `M`. If `m` is a
subadditive function (`m (a + b) ≤ m a + m b`) preserved under division by a natural, `f` is a
function valued in that subsemigroup and `s` is a nonempty set, then
`m (𝔼 i ∈ s, f i) ≤ 𝔼 i ∈ s, m (f i)`. -/
theorem le_expect_nonempty_of_subadditive_on_pred (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_nonempty : s.Nonempty) (hs : ∀ i ∈ s, p (f i)) : m (𝔼 i ∈ s, f i) ≤ 𝔼 i ∈ s, m (f i) :=
by
simp only [expect, h_div _ _ (sum_induction_nonempty _ _ hp_add hs_nonempty hs)]
exact
smul_le_smul_of_nonneg_left (le_sum_nonempty_of_subadditive_on_pred _ _ h_add hp_add _ _ hs_nonempty hs) <| by
positivity
