Mathlib.Algebra.Order.BigOperators.Group.Multiset

Multiset.one_le_prod_of_one_le theorem

: (∀ x ∈ s, (1 : α) ≤ x) → 1 ≤ s.prod

Full source

@[to_additive sum_nonneg]
lemma one_le_prod_of_one_le : (∀ x ∈ s, (1 : α) ≤ x) → 1 ≤ s.prod :=
  Quotient.inductionOn s fun l hl => by simpa using List.one_le_prod_of_one_le hl

Product Lower Bound in Ordered Monoid: $1 \leq \prod s$

Informal description

Let $s$ be a multiset in an ordered monoid $\alpha$ such that every element $x \in s$ satisfies $1 \leq x$. Then the product of all elements in $s$ is bounded below by $1$, i.e., $1 \leq \prod s$.

Multiset.single_le_prod theorem

: (∀ x ∈ s, (1 : α) ≤ x) → ∀ x ∈ s, x ≤ s.prod

Full source

@[to_additive]
lemma single_le_prod : (∀ x ∈ s, (1 : α) ≤ x) → ∀ x ∈ s, x ≤ s.prod :=
  Quotient.inductionOn s fun l hl x hx => by simpa using List.single_le_prod hl x hx

Element-wise Lower Bound Implies Product Upper Bound in Ordered Monoid

Informal description

Let $s$ be a multiset in an ordered monoid $\alpha$ such that every element $x \in s$ satisfies $1 \leq x$. Then for any element $x \in s$, we have $x \leq \prod s$.

Multiset.prod_le_pow_card theorem

(s : Multiset α) (n : α) (h : ∀ x ∈ s, x ≤ n) : s.prod ≤ n ^ card s

Full source

@[to_additive sum_le_card_nsmul]
lemma prod_le_pow_card (s : Multiset α) (n : α) (h : ∀ x ∈ s, x ≤ n) : s.prod ≤ n ^ card s := by
  induction s using Quotient.inductionOn
  simpa using List.prod_le_pow_card _ _ h

Product Bound in Ordered Monoid: $\prod s \leq n^{|s|}$

Informal description

Let $s$ be a multiset in an ordered monoid $\alpha$ and let $n \in \alpha$ be such that every element $x \in s$ satisfies $x \leq n$. Then the product of all elements in $s$ is bounded above by $n$ raised to the power of the cardinality of $s$, i.e., $\prod s \leq n^{|s|}$.

Multiset.all_one_of_le_one_le_of_prod_eq_one theorem

: (∀ x ∈ s, (1 : α) ≤ x) → s.prod = 1 → ∀ x ∈ s, x = (1 : α)

Full source

@[to_additive all_zero_of_le_zero_le_of_sum_eq_zero]
lemma all_one_of_le_one_le_of_prod_eq_one :
    (∀ x ∈ s, (1 : α) ≤ x) → s.prod = 1 → ∀ x ∈ s, x = (1 : α) :=
  Quotient.inductionOn s (by
    simp only [quot_mk_to_coe, prod_coe, mem_coe]
    exact fun l => List.all_one_of_le_one_le_of_prod_eq_one)

Elements in Ordered Monoid Multiset with Product One are All One

Informal description

Let $s$ be a multiset in an ordered monoid $\alpha$ such that every element $x \in s$ satisfies $1 \leq x$. If the product of all elements in $s$ equals $1$, then every element in $s$ must be equal to $1$.

Multiset.prod_le_prod_of_rel_le theorem

(h : s.Rel (· ≤ ·) t) : s.prod ≤ t.prod

Full source

@[to_additive]
lemma prod_le_prod_of_rel_le (h : s.Rel (· ≤ ·) t) : s.prod ≤ t.prod := by
  induction h with
  | zero => rfl
  | cons rh _ rt =>
    rw [prod_cons, prod_cons]
    exact mul_le_mul' rh rt

Product Inequality for Relationally Ordered Multisets: $\prod s \leq \prod t$

Informal description

Let $s$ and $t$ be multisets in an ordered monoid $\alpha$ such that there exists a relation-preserving pairing between their elements where each element of $s$ is less than or equal to its corresponding element in $t$. Then the product of all elements in $s$ is less than or equal to the product of all elements in $t$, i.e., $\prod s \leq \prod t$.

Multiset.prod_map_le_prod_map theorem

 {s : Multiset ι} (f : ι → α) (g : ι → α) (h : ∀ i, i ∈ s → f i ≤ g i) : (s.map f).prod ≤ (s.map g).prod

Full source

@[to_additive]
lemma prod_map_le_prod_map {s : Multiset ι} (f : ι → α) (g : ι → α) (h : ∀ i, i ∈ s → f i ≤ g i) :
    (s.map f).prod ≤ (s.map g).prod :=
  prod_le_prod_of_rel_le <| rel_map.2 <| rel_refl_of_refl_on h

Monotonicity of Multiset Product under Pointwise Inequality: $\prod_{i \in s} f(i) \leq \prod_{i \in s} g(i)$

Informal description

Let $s$ be a multiset over an index type $\iota$, and let $f, g : \iota \to \alpha$ be functions into an ordered monoid $\alpha$. If for every $i \in s$ we have $f(i) \leq g(i)$, then the product of the elements in the multiset obtained by applying $f$ to each element of $s$ is less than or equal to the product of the elements in the multiset obtained by applying $g$ to each element of $s$, i.e., $\prod_{i \in s} f(i) \leq \prod_{i \in s} g(i)$.

Multiset.prod_map_le_prod theorem

(f : α → α) (h : ∀ x, x ∈ s → f x ≤ x) : (s.map f).prod ≤ s.prod

Full source

@[to_additive]
lemma prod_map_le_prod (f : α → α) (h : ∀ x, x ∈ s → f x ≤ x) : (s.map f).prod ≤ s.prod :=
  prod_le_prod_of_rel_le <| rel_map_left.2 <| rel_refl_of_refl_on h

Product Inequality for Monotone Function on Multiset: $\prod (f \circ s) \leq \prod s$

Informal description

Let $s$ be a multiset in an ordered monoid $\alpha$ and $f : \alpha \to \alpha$ be a function such that for every $x \in s$, $f(x) \leq x$. Then the product of the multiset obtained by applying $f$ to each element of $s$ is less than or equal to the product of $s$, i.e., $\prod (s.map\, f) \leq \prod s$.

Multiset.prod_le_prod_map theorem

(f : α → α) (h : ∀ x, x ∈ s → x ≤ f x) : s.prod ≤ (s.map f).prod

Full source

@[to_additive]
lemma prod_le_prod_map (f : α → α) (h : ∀ x, x ∈ s → x ≤ f x) : s.prod ≤ (s.map f).prod :=
  prod_map_le_prod (α := αᵒᵈ) f h

Product Inequality for Monotone Function on Multiset: $\prod s \leq \prod (f \circ s)$

Informal description

Let $s$ be a multiset in an ordered monoid $\alpha$ and $f : \alpha \to \alpha$ be a function such that for every $x \in s$, $x \leq f(x)$. Then the product of $s$ is less than or equal to the product of the multiset obtained by applying $f$ to each element of $s$, i.e., $\prod s \leq \prod (s.map\, f)$.

Multiset.pow_card_le_prod theorem

(h : ∀ x ∈ s, a ≤ x) : a ^ card s ≤ s.prod

Full source

@[to_additive card_nsmul_le_sum]
lemma pow_card_le_prod (h : ∀ x ∈ s, a ≤ x) : a ^ card s ≤ s.prod := by
  rw [← Multiset.prod_replicate, ← Multiset.map_const]
  exact prod_map_le_prod _ h

Power-Cardinality Inequality for Multiset Products: $a^{|s|} \leq \prod s$

Informal description

Let $s$ be a multiset in an ordered monoid $\alpha$ and let $a \in \alpha$ be such that $a \leq x$ for every $x \in s$. Then $a^{|s|} \leq \prod s$, where $|s|$ denotes the cardinality of $s$ and $\prod s$ denotes the product of all elements in $s$.

Multiset.le_prod_of_submultiplicative_on_pred theorem

 (f : α → β) (p : α → Prop) (h_one : f 1 = 1) (hp_one : p 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

@[to_additive le_sum_of_subadditive_on_pred]
lemma le_prod_of_submultiplicative_on_pred (f : α → β)
    (p : α → Prop) (h_one : f 1 = 1) (hp_one : p 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 ?_ ?_
  · simp [le_of_eq h_one]
  intro a s hs hpsa
  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 p s hp_mul hp_one 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_left' (hs hps) _)

Submultiplicative Inequality for Multiset Products with Predicate

Informal description

Let $\alpha$ and $\beta$ be ordered monoids, $f : \alpha \to \beta$ a function, and $p : \alpha \to \text{Prop}$ a predicate on $\alpha$. Suppose that: 1. $f(1) = 1$ and $p(1)$ holds, 2. For all $a, b \in \alpha$, if $p(a)$ and $p(b)$ hold, then $f(a \cdot b) \leq f(a) \cdot f(b)$, 3. For all $a, b \in \alpha$, if $p(a)$ and $p(b)$ hold, then $p(a \cdot b)$ holds, 4. Every element $a$ in the multiset $s$ satisfies $p(a)$. Then, $f(\prod s) \leq \prod_{a \in s} f(a)$.

Multiset.le_prod_of_submultiplicative theorem

 (f : α → β) (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

@[to_additive le_sum_of_subadditive]
lemma le_prod_of_submultiplicative (f : α → β) (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 f (fun _ => True) h_one trivial (fun x y _ _ => h_mul x y)
    (by simp) s (by simp)

Submultiplicative Inequality for Multiset Products

Informal description

Let $\alpha$ and $\beta$ be ordered monoids and $f : \alpha \to \beta$ a function such that: 1. $f(1) = 1$, 2. For all $a, b \in \alpha$, $f(a \cdot b) \leq f(a) \cdot f(b)$. Then for any multiset $s$ of elements in $\alpha$, we have $f(\prod s) \leq \prod_{a \in s} f(a)$.

Multiset.le_prod_nonempty_of_submultiplicative_on_pred theorem

 (f : α → β) (p : α → Prop) (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 α) (hs_nonempty : s ≠ ∅) (hs : ∀ a, a ∈ s → p a) : f s.prod ≤ (s.map f).prod

Full source

@[to_additive le_sum_nonempty_of_subadditive_on_pred]
lemma le_prod_nonempty_of_submultiplicative_on_pred (f : α → β) (p : α → Prop)
    (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 α) (hs_nonempty : s ≠ ∅) (hs : ∀ a, a ∈ s → p a) : f s.prod ≤ (s.map f).prod := by
  revert s
  refine Multiset.induction ?_ ?_
  · simp
  rintro a s hs - hsa_prop
  rw [prod_cons, map_cons, prod_cons]
  by_cases hs_empty : s = ∅
  · simp [hs_empty]
  have hsa_restrict : ∀ x, x ∈ s → p x := fun x hx => hsa_prop x (mem_cons_of_mem hx)
  have hp_sup : p s.prod := prod_induction_nonempty p hp_mul hs_empty hsa_restrict
  have hp_a : p a := hsa_prop a (mem_cons_self a s)
  exact (h_mul a _ hp_a hp_sup).trans (mul_le_mul_left' (hs hs_empty hsa_restrict) _)

Submultiplicative Inequality for Nonempty Multisets with Predicate

Informal description

Let $\alpha$ and $\beta$ be ordered monoids, $f : \alpha \to \beta$ a function, and $p : \alpha \to \text{Prop}$ a predicate on $\alpha$. Suppose that: 1. For all $a, b \in \alpha$, if $p(a)$ and $p(b)$ hold, then $f(a \cdot b) \leq f(a) \cdot f(b)$. 2. For all $a, b \in \alpha$, if $p(a)$ and $p(b)$ hold, then $p(a \cdot b)$ holds. 3. The multiset $s$ is nonempty and every element $a \in s$ satisfies $p(a)$. Then, $f(\prod s) \leq \prod_{a \in s} f(a)$.

Multiset.le_prod_nonempty_of_submultiplicative theorem

 (f : α → β) (h_mul : ∀ a b, f (a * b) ≤ f a * f b) (s : Multiset α) (hs_nonempty : s ≠ ∅) : f s.prod ≤ (s.map f).prod

Full source

@[to_additive le_sum_nonempty_of_subadditive]
lemma le_prod_nonempty_of_submultiplicative (f : α → β) (h_mul : ∀ a b, f (a * b) ≤ f a * f b)
    (s : Multiset α) (hs_nonempty : s ≠ ∅) : f s.prod ≤ (s.map f).prod :=
  le_prod_nonempty_of_submultiplicative_on_pred f (fun _ => True) (by simp [h_mul]) (by simp) s
    hs_nonempty (by simp)

Submultiplicative Inequality for Nonempty Multiset Products

Informal description

Let $\alpha$ and $\beta$ be ordered monoids and $f : \alpha \to \beta$ a function such that for all $a, b \in \alpha$, $f(a \cdot b) \leq f(a) \cdot f(b)$. Then for any nonempty multiset $s$ of elements in $\alpha$, we have $f(\prod s) \leq \prod_{a \in s} f(a)$.

Multiset.prod_lt_prod' theorem

(hle : ∀ i ∈ s, f i ≤ g i) (hlt : ∃ i ∈ s, f i < g i) : (s.map f).prod < (s.map g).prod

Full source

@[to_additive sum_lt_sum]
lemma prod_lt_prod' (hle : ∀ i ∈ s, f i ≤ g i) (hlt : ∃ i ∈ s, f i < g i) :
    (s.map f).prod < (s.map g).prod := by
  obtain ⟨l⟩ := s
  simp only [Multiset.quot_mk_to_coe'', Multiset.map_coe, Multiset.prod_coe]
  exact List.prod_lt_prod' f g hle hlt

Strict Product Inequality for Multisets in Ordered Cancellative Monoids

Informal description

Let $\alpha$ be an ordered cancellative monoid and $s$ a multiset of elements in $\alpha$. Given two functions $f, g : \alpha \to \alpha$ such that: 1. For all $i \in s$, $f(i) \leq g(i)$, and 2. There exists some $i \in s$ such that $f(i) < g(i)$, then the product of the images of $f$ over $s$ is strictly less than the product of the images of $g$ over $s$, i.e., $\prod_{i \in s} f(i) < \prod_{i \in s} g(i)$.

Multiset.prod_lt_prod_of_nonempty' theorem

(hs : s ≠ ∅) (hfg : ∀ i ∈ s, f i < g i) : (s.map f).prod < (s.map g).prod

Full source

@[to_additive sum_lt_sum_of_nonempty]
lemma prod_lt_prod_of_nonempty' (hs : s ≠ ∅) (hfg : ∀ i ∈ s, f i < g i) :
    (s.map f).prod < (s.map g).prod := by
  obtain ⟨i, hi⟩ := exists_mem_of_ne_zero hs
  exact prod_lt_prod' (fun i hi => le_of_lt (hfg i hi)) ⟨i, hi, hfg i hi⟩

Strict Product Inequality for Nonempty Multisets in Ordered Cancellative Monoids

Informal description

Let $\alpha$ be an ordered cancellative monoid and $s$ a nonempty multiset of elements in $\alpha$. Given two functions $f, g : \alpha \to \alpha$ such that for all $i \in s$, $f(i) < g(i)$, then the product of the images of $f$ over $s$ is strictly less than the product of the images of $g$ over $s$, i.e., $\prod_{i \in s} f(i) < \prod_{i \in s} g(i)$.

Multiset.prod_eq_one_iff theorem

[IsOrderedMonoid α] : m.prod = 1 ↔ ∀ x ∈ m, x = (1 : α)

Full source

@[to_additive] lemma prod_eq_one_iff [IsOrderedMonoid α] : m.prod = 1 ↔ ∀ x ∈ m, x = (1 : α) :=
  Quotient.inductionOn m fun l ↦ by simpa using List.prod_eq_one_iff

Product of Multiset Elements Equals One if and only if All Elements Are One in Ordered Monoid

Informal description

Let $\alpha$ be an ordered monoid and $m$ be a multiset of elements in $\alpha$. The product of all elements in $m$ equals the multiplicative identity $1$ if and only if every element in $m$ is equal to $1$.

Multiset.le_prod_of_mem theorem

(ha : a ∈ m) : a ≤ m.prod

Full source

@[to_additive] lemma le_prod_of_mem (ha : a ∈ m) : a ≤ m.prod := by
  obtain ⟨t, rfl⟩ := exists_cons_of_mem ha
  rw [prod_cons]
  exact _root_.le_mul_right (le_refl a)

Element of Multiset is Bounded by its Product in Ordered Monoid

Informal description

Let $\alpha$ be a canonically ordered multiplicative monoid and $m$ be a multiset of elements in $\alpha$. For any element $a \in m$, we have $a \leq \prod m$, where $\prod m$ denotes the product of all elements in $m$.

Multiset.max_le_of_forall_le theorem

 {α : Type*} [LinearOrder α] [OrderBot α] (l : Multiset α) (n : α) (h : ∀ x ∈ l, x ≤ n) : l.fold max ⊥ ≤ n

Full source

lemma max_le_of_forall_le {α : Type*} [LinearOrder α] [OrderBot α] (l : Multiset α)
    (n : α) (h : ∀ x ∈ l, x ≤ n) : l.fold max ⊥ ≤ n := by
  induction l using Quotient.inductionOn
  simpa using List.max_le_of_forall_le _ _ h

Maximum of Multiset Elements Bounded Above by Common Upper Bound

Informal description

Let $\alpha$ be a linearly ordered type with a least element $\bot$, and let $l$ be a multiset of elements in $\alpha$. If every element $x$ in $l$ satisfies $x \leq n$ for some fixed $n \in \alpha$, then the maximum of all elements in $l$ (computed via folding with $\max$ starting from $\bot$) is also less than or equal to $n$. In other words, if $\forall x \in l, x \leq n$, then $\text{fold}\ \max\ \bot\ l \leq n$.

Multiset.max_prod_le theorem

 [CommMonoid α] [LinearOrder α] [IsOrderedMonoid α] {s : Multiset ι} {f g : ι → α} :
  max (s.map f).prod (s.map g).prod ≤ (s.map fun i ↦ max (f i) (g i)).prod

Full source

@[to_additive]
lemma max_prod_le [CommMonoid α] [LinearOrder α] [IsOrderedMonoid α]
    {s : Multiset ι} {f g : ι → α} :
    max (s.map f).prod (s.map g).prod ≤ (s.map fun i ↦ max (f i) (g i)).prod := by
  obtain ⟨l⟩ := s
  simp_rw [Multiset.quot_mk_to_coe'', Multiset.map_coe, Multiset.prod_coe]
  apply List.max_prod_le

Maximum of Products is Bounded by Product of Maxima in Ordered Monoids

Informal description

Let $\alpha$ be a commutative monoid with a linear order that forms an ordered monoid, and let $s$ be a multiset over an index type $\iota$. For any two functions $f, g : \iota \to \alpha$, the maximum of the products of $f$ and $g$ over $s$ is less than or equal to the product over $s$ of the pointwise maxima of $f$ and $g$. That is, \[ \max\left(\prod_{x \in s} f(x), \prod_{x \in s} g(x)\right) \leq \prod_{x \in s} \max(f(x), g(x)). \]

Multiset.prod_min_le theorem

 [CommMonoid α] [LinearOrder α] [IsOrderedMonoid α] {s : Multiset ι} {f g : ι → α} :
  (s.map fun i ↦ min (f i) (g i)).prod ≤ min (s.map f).prod (s.map g).prod

Full source

@[to_additive]
lemma prod_min_le [CommMonoid α] [LinearOrder α] [IsOrderedMonoid α]
    {s : Multiset ι} {f g : ι → α} :
    (s.map fun i ↦ min (f i) (g i)).prod ≤ min (s.map f).prod (s.map g).prod := by
  obtain ⟨l⟩ := s
  simp_rw [Multiset.quot_mk_to_coe'', Multiset.map_coe, Multiset.prod_coe]
  apply List.prod_min_le

Product of Pointwise Minima is Bounded by Minimum of Products in Ordered Monoids

Informal description

Let $\alpha$ be a commutative monoid with a linear order such that multiplication is monotone in both arguments. For any multiset $s$ over an index type $\iota$ and any functions $f, g : \iota \to \alpha$, the product of the pointwise minima $\prod_{i \in s} \min(f(i), g(i))$ is less than or equal to the minimum of the products $\min\left(\prod_{i \in s} f(i), \prod_{i \in s} g(i)\right)$.

Multiset.abs_sum_le_sum_abs theorem

[AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] {s : Multiset α} : |s.sum| ≤ (s.map abs).sum

Full source

lemma abs_sum_le_sum_abs [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] {s : Multiset α} :
    |s.sum| ≤ (s.map abs).sum :=
  le_sum_of_subadditive _ abs_zero abs_add s

Absolute Value of Sum is Bounded by Sum of Absolute Values in Ordered Additive Monoids

Informal description

Let $\alpha$ be an additive commutative group with a linear order that forms an ordered additive monoid. For any multiset $s$ of elements in $\alpha$, the absolute value of the sum of $s$ is less than or equal to the sum of the absolute values of the elements in $s$, i.e., \[ \left| \sum_{x \in s} x \right| \leq \sum_{x \in s} |x|. \]