Theorems · Theorem · order theory

Finset.le_expect_nonempty_of_subadditive_on_pred

∀ {ι : Type u_1} {M : Type u_4} {N : Type u_5} [inst : AddCommMonoid M] [inst_1 : Module ℚ≥0 M]
  [inst_2 : AddCommMonoid N] [inst_3 : PartialOrder N] [IsOrderedAddMonoid N] [inst_5 : Module ℚ≥0 N]
  [PosSMulMono ℚ≥0 N] {m : M → N} {p : M → Prop} {f : ι → M} {s : Finset ι},
  (∀ (a b : M), p a → p b → m (a + b) ≤ m a + m b) →
    (∀ (a b : M), p a → p b → p (a + b)) →
      (∀ (n : ℕ) (a : M), p a → m ((↑n)⁻¹ • a) = (↑n)⁻¹ • m a) →
        s.Nonempty → (∀ i ∈ s, p (f i)) → m (s.expect fun i => f i) ≤ s.expect fun i => m (f i)

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).

Defined in

Mathlib.Algebra.Order.BigOperators.Expect

Cited by

2 results in Mathlib

Foundations

Depth 91 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddCommMonoidModuleAddCommMonoidPartialOrderIsOrderedAddMonoidModulePosSMulMono