Mathlib.Algebra.Order.BigOperators.Ring.Multiset

Module docstring

{"# Big operators on a multiset in ordered rings

This file contains the results concerning the interaction of multiset big operators with ordered rings. "}

CanonicallyOrderedAdd.multiset_prod_pos theorem

 {R : Type*} [CommSemiring R] [PartialOrder R] [CanonicallyOrderedAdd R] [NoZeroDivisors R] [Nontrivial R]
  {m : Multiset R} : 0 < m.prod ↔ ∀ x ∈ m, 0 < x

Full source

@[simp]
lemma CanonicallyOrderedAdd.multiset_prod_pos {R : Type*}
    [CommSemiring R] [PartialOrder R] [CanonicallyOrderedAdd R] [NoZeroDivisors R] [Nontrivial R]
    {m : Multiset R} : 0 < m.prod ↔ ∀ x ∈ m, 0 < x := by
  rcases m with ⟨l⟩
  rw [Multiset.quot_mk_to_coe'', Multiset.prod_coe]
  exact CanonicallyOrderedAdd.list_prod_pos

Positivity of Multiset Product in Canonically Ordered Semiring

Informal description

Let $R$ be a commutative semiring with a partial order, which is canonically ordered with respect to addition, has no zero divisors, and is nontrivial. For any multiset $m$ of elements in $R$, the product of all elements in $m$ is positive if and only if every element in $m$ is positive.

Multiset.le_prod_of_submultiplicative_on_pred_of_nonneg theorem

 (f : α → β) (p : α → Prop) (h0 : ∀ a, 0 ≤ f a) (h_one : f 1 ≤ 1) (h_mul : ∀ a b, p a → p b → f (a * b) ≤ f a * f b)
  (hp_mul : ∀ a b, p a → p b → p (a * b)) (s : Multiset α) (hps : ∀ a, a ∈ s → p a) : f s.prod ≤ (s.map f).prod

Full source

theorem Multiset.le_prod_of_submultiplicative_on_pred_of_nonneg (f : α → β) (p : α → Prop)
    (h0 : ∀ a, 0 ≤ f a) (h_one : f 1 ≤ 1) (h_mul : ∀ a b, p a → p b → f (a * b) ≤ f a * f b)
    (hp_mul : ∀ a b, p a → p b → p (a * b)) (s : Multiset α) (hps : ∀ a, a ∈ s → p a) :
    f s.prod ≤ (s.map f).prod := by
  revert s
  refine Multiset.induction (by simp [h_one]) ?_
  intro a s hs hpsa
  by_cases hs0 : s = ∅
  · simp [hs0]
  · have hps : ∀ x, x ∈ s → p x := fun x hx ↦ hpsa x (mem_cons_of_mem hx)
    have hp_prod : p s.prod := prod_induction_nonempty p hp_mul hs0 hps
    rw [prod_cons, map_cons, prod_cons]
    exact (h_mul a s.prod (hpsa a (mem_cons_self a s)) hp_prod).trans
      (mul_le_mul_of_nonneg_left (hs hps) (h0 _))

Submultiplicative Inequality for Multiset Product under Predicate and Nonnegativity Conditions

Informal description

Let $\alpha$ and $\beta$ be types with a multiplication operation and a partial order. Given a function $f \colon \alpha \to \beta$ and a predicate $p$ on $\alpha$ satisfying: 1. $f(a) \geq 0$ for all $a \in \alpha$, 2. $f(1) \leq 1$, 3. $f(a \cdot b) \leq f(a) \cdot f(b)$ for all $a, b \in \alpha$ such that $p(a)$ and $p(b)$ hold, 4. $p(a \cdot b)$ holds whenever $p(a)$ and $p(b)$ hold, then for any multiset $s$ of elements in $\alpha$ where $p(a)$ holds for all $a \in s$, we have \[ f\left(\prod_{a \in s} a\right) \leq \prod_{a \in s} f(a). \]

Multiset.le_prod_of_submultiplicative_of_nonneg theorem

 (f : α → β) (h0 : ∀ a, 0 ≤ f a) (h_one : f 1 ≤ 1) (h_mul : ∀ a b, f (a * b) ≤ f a * f b) (s : Multiset α) :
  f s.prod ≤ (s.map f).prod

Full source

theorem Multiset.le_prod_of_submultiplicative_of_nonneg (f : α → β) (h0 : ∀ a, 0 ≤ f a)
    (h_one : f 1 ≤ 1) (h_mul : ∀ a b, f (a * b) ≤ f a * f b) (s : Multiset α) :
    f s.prod ≤ (s.map f).prod :=
  le_prod_of_submultiplicative_on_pred_of_nonneg f (fun _ ↦ True) h0 h_one
    (fun x y _ _ ↦ h_mul x y) (by simp) s (by simp)

Submultiplicative Inequality for Multiset Product with Nonnegativity Conditions

Informal description

Let $\alpha$ and $\beta$ be types equipped with multiplication and a partial order. Given a function $f \colon \alpha \to \beta$ satisfying: 1. $f(a) \geq 0$ for all $a \in \alpha$, 2. $f(1) \leq 1$, 3. $f(a \cdot b) \leq f(a) \cdot f(b)$ for all $a, b \in \alpha$, then for any multiset $s$ of elements in $\alpha$, we have \[ f\left(\prod_{a \in s} a\right) \leq \prod_{a \in s} f(a). \]