Mathlib.Algebra.Order.BigOperators.Group.List

List.Forall₂.prod_le_prod' theorem

 [Preorder M] [MulRightMono M] [MulLeftMono M] {l₁ l₂ : List M} (h : Forall₂ (· ≤ ·) l₁ l₂) : l₁.prod ≤ l₂.prod

Full source

@[to_additive sum_le_sum]
lemma Forall₂.prod_le_prod' [Preorder M] [MulRightMono M]
    [MulLeftMono M] {l₁ l₂ : List M} (h : Forall₂ (· ≤ ·) l₁ l₂) :
    l₁.prod ≤ l₂.prod := by
  induction h with
  | nil => rfl
  | cons hab ih ih' => simpa only [prod_cons] using mul_le_mul' hab ih'

Product Inequality for Pairwise Ordered Lists in Monoids

Informal description

Let $M$ be a preordered monoid where multiplication is monotone in both arguments. For any two lists $l_1$ and $l_2$ of elements in $M$, if there exists a pairwise inequality $h : \text{Forall}_2 (\leq) l_1 l_2$ (meaning each element of $l_1$ is less than or equal to the corresponding element in $l_2$), then the product of elements in $l_1$ is less than or equal to the product of elements in $l_2$.

List.Sublist.prod_le_prod' theorem

 [Preorder M] [MulRightMono M] [MulLeftMono M] {l₁ l₂ : List M} (h : l₁ <+ l₂) (h₁ : ∀ a ∈ l₂, (1 : M) ≤ a) :
  l₁.prod ≤ l₂.prod

Full source

/-- If `l₁` is a sublist of `l₂` and all elements of `l₂` are greater than or equal to one, then
`l₁.prod ≤ l₂.prod`. One can prove a stronger version assuming `∀ a ∈ l₂.diff l₁, 1 ≤ a` instead
of `∀ a ∈ l₂, 1 ≤ a` but this lemma is not yet in `mathlib`. -/
@[to_additive sum_le_sum "If `l₁` is a sublist of `l₂` and all elements of `l₂` are nonnegative,
  then `l₁.sum ≤ l₂.sum`.
  One can prove a stronger version assuming `∀ a ∈ l₂.diff l₁, 0 ≤ a` instead of `∀ a ∈ l₂, 0 ≤ a`
  but this lemma is not yet in `mathlib`."]
lemma Sublist.prod_le_prod' [Preorder M] [MulRightMono M]
    [MulLeftMono M] {l₁ l₂ : List M} (h : l₁ <+ l₂)
    (h₁ : ∀ a ∈ l₂, (1 : M) ≤ a) : l₁.prod ≤ l₂.prod := by
  induction h with
  | slnil => rfl
  | cons a _ ih' =>
    simp only [prod_cons, forall_mem_cons] at h₁ ⊢
    exact (ih' h₁.2).trans (le_mul_of_one_le_left' h₁.1)
  | cons₂ a _ ih' =>
    simp only [prod_cons, forall_mem_cons] at h₁ ⊢
    exact mul_le_mul_left' (ih' h₁.2) _

Product Inequality for Sublists in Ordered Monoids

Informal description

Let $M$ be a preordered monoid where multiplication is monotone in both arguments. For any two lists $l_1$ and $l_2$ of elements in $M$, if $l_1$ is a sublist of $l_2$ and every element of $l_2$ is greater than or equal to the multiplicative identity $1$, then the product of elements in $l_1$ is less than or equal to the product of elements in $l_2$.

List.SublistForall₂.prod_le_prod' theorem

 [Preorder M] [MulRightMono M] [MulLeftMono M] {l₁ l₂ : List M} (h : SublistForall₂ (· ≤ ·) l₁ l₂)
  (h₁ : ∀ a ∈ l₂, (1 : M) ≤ a) : l₁.prod ≤ l₂.prod

Full source

@[to_additive sum_le_sum]
lemma SublistForall₂.prod_le_prod' [Preorder M]
    [MulRightMono M] [MulLeftMono M]
    {l₁ l₂ : List M} (h : SublistForall₂ (· ≤ ·) l₁ l₂) (h₁ : ∀ a ∈ l₂, (1 : M) ≤ a) :
    l₁.prod ≤ l₂.prod :=
  let ⟨_, hall, hsub⟩ := sublistForall₂_iff.1 h
  hall.prod_le_prod'.trans <| hsub.prod_le_prod' h₁

Product Inequality for Sublists with Pairwise Ordering in Ordered Monoids

Informal description

Let $M$ be a preordered monoid where multiplication is monotone in both arguments. For any two lists $l_1$ and $l_2$ of elements in $M$, if $l_1$ is a sublist of $l_2$ with a pairwise inequality (i.e., each element of $l_1$ is less than or equal to the corresponding element in $l_2$ via the relation $\text{SublistForall}_2 (\leq)$), and every element of $l_2$ is greater than or equal to the multiplicative identity $1$, then the product of elements in $l_1$ is less than or equal to the product of elements in $l_2$.

List.prod_le_prod' theorem

 [Preorder M] [MulRightMono M] [MulLeftMono M] {l : List ι} {f g : ι → M} (h : ∀ i ∈ l, f i ≤ g i) :
  (l.map f).prod ≤ (l.map g).prod

Full source

@[to_additive sum_le_sum]
lemma prod_le_prod' [Preorder M] [MulRightMono M]
    [MulLeftMono M] {l : List ι} {f g : ι → M} (h : ∀ i ∈ l, f i ≤ g i) :
    (l.map f).prod ≤ (l.map g).prod :=
  Forall₂.prod_le_prod' <| by simpa

Monotonicity of List Product under Pointwise Inequality

Informal description

Let $M$ be a preordered monoid where multiplication is monotone in both arguments. For any list $l$ of elements in a type $\iota$, and for any two functions $f, g : \iota \to M$ such that $f(i) \leq g(i)$ for all $i \in l$, the product of the mapped values $\prod_{i \in l} f(i)$ is less than or equal to the product of the mapped values $\prod_{i \in l} g(i)$.

List.prod_lt_prod' theorem

 [Preorder M] [MulLeftStrictMono M] [MulLeftMono M] [MulRightStrictMono M] [MulRightMono M] {l : List ι} (f g : ι → M)
  (h₁ : ∀ i ∈ l, f i ≤ g i) (h₂ : ∃ i ∈ l, f i < g i) : (l.map f).prod < (l.map g).prod

Full source

@[to_additive sum_lt_sum]
lemma prod_lt_prod' [Preorder M] [MulLeftStrictMono M]
    [MulLeftMono M] [MulRightStrictMono M]
    [MulRightMono M] {l : List ι} (f g : ι → M)
    (h₁ : ∀ i ∈ l, f i ≤ g i) (h₂ : ∃ i ∈ l, f i < g i) : (l.map f).prod < (l.map g).prod := by
  induction' l with i l ihl
  · rcases h₂ with ⟨_, ⟨⟩, _⟩
  simp only [forall_mem_cons, map_cons, prod_cons] at h₁ ⊢
  simp only [mem_cons, exists_eq_or_imp] at h₂
  cases h₂
  · exact mul_lt_mul_of_lt_of_le ‹_› (prod_le_prod' h₁.2)
  · exact mul_lt_mul_of_le_of_lt h₁.1 <| ihl h₁.2 ‹_›

Strict Monotonicity of List Product under Pointwise Inequality with Strictness Condition

Informal description

Let $M$ be a preordered monoid where multiplication is strictly monotone in both arguments. For any list $l$ of elements in a type $\iota$, and for any two functions $f, g : \iota \to M$ such that: 1. $f(i) \leq g(i)$ for all $i \in l$, and 2. there exists some $i \in l$ with $f(i) < g(i)$, then the product of the mapped values $\prod_{i \in l} f(i)$ is strictly less than the product of the mapped values $\prod_{i \in l} g(i)$.

List.prod_lt_prod_of_ne_nil theorem

 [Preorder M] [MulLeftStrictMono M] [MulLeftMono M] [MulRightStrictMono M] [MulRightMono M] {l : List ι} (hl : l ≠ [])
  (f g : ι → M) (hlt : ∀ i ∈ l, f i < g i) : (l.map f).prod < (l.map g).prod

Full source

@[to_additive]
lemma prod_lt_prod_of_ne_nil [Preorder M] [MulLeftStrictMono M]
    [MulLeftMono M] [MulRightStrictMono M]
    [MulRightMono M] {l : List ι} (hl : l ≠ []) (f g : ι → M)
    (hlt : ∀ i ∈ l, f i < g i) : (l.map f).prod < (l.map g).prod :=
  (prod_lt_prod' f g fun i hi => (hlt i hi).le) <|
    (exists_mem_of_ne_nil l hl).imp fun i hi => ⟨hi, hlt i hi⟩

Strict Monotonicity of List Product for Non-Empty Lists under Strict Pointwise Inequality

Informal description

Let $M$ be a preordered monoid where multiplication is strictly monotone in both arguments. For any non-empty list $l$ of elements in a type $\iota$, and for any two functions $f, g : \iota \to M$ such that $f(i) < g(i)$ for all $i \in l$, the product of the mapped values $\prod_{i \in l} f(i)$ is strictly less than the product of the mapped values $\prod_{i \in l} g(i)$.

List.prod_le_pow_card theorem

[Preorder M] [MulRightMono M] [MulLeftMono M] (l : List M) (n : M) (h : ∀ x ∈ l, x ≤ n) : l.prod ≤ n ^ l.length

Full source

@[to_additive sum_le_card_nsmul]
lemma prod_le_pow_card [Preorder M] [MulRightMono M]
    [MulLeftMono M] (l : List M) (n : M) (h : ∀ x ∈ l, x ≤ n) :
    l.prod ≤ n ^ l.length := by
  simpa only [map_id', map_const', prod_replicate] using prod_le_prod' h

Product of List Elements Bounded by Power of Upper Bound

Informal description

Let $M$ be a preordered monoid where multiplication is monotone in both arguments. For any list $l$ of elements in $M$ and any element $n \in M$ such that $x \leq n$ for all $x \in l$, the product of the elements in $l$ is less than or equal to $n$ raised to the power of the length of $l$, i.e., $\prod_{x \in l} x \leq n^{|l|}$.

List.pow_card_le_prod theorem

[Preorder M] [MulRightMono M] [MulLeftMono M] (l : List M) (n : M) (h : ∀ x ∈ l, n ≤ x) : n ^ l.length ≤ l.prod

Full source

@[to_additive card_nsmul_le_sum]
lemma pow_card_le_prod [Preorder M] [MulRightMono M]
    [MulLeftMono M] (l : List M) (n : M) (h : ∀ x ∈ l, n ≤ x) :
    n ^ l.length ≤ l.prod :=
  @prod_le_pow_card Mᵒᵈ _ _ _ _ l n h

Lower Bound on Product of List Elements via Power of Lower Bound

Informal description

Let $M$ be a preordered monoid where multiplication is monotone in both arguments. For any list $l$ of elements in $M$ and any element $n \in M$ such that $n \leq x$ for all $x \in l$, the power $n^{|l|}$ is less than or equal to the product of the elements in $l$, i.e., $n^{|l|} \leq \prod_{x \in l} x$.

List.exists_lt_of_prod_lt' theorem

 [LinearOrder M] [MulRightMono M] [MulLeftMono M] {l : List ι} (f g : ι → M) (h : (l.map f).prod < (l.map g).prod) :
  ∃ i ∈ l, f i < g i

Full source

@[to_additive exists_lt_of_sum_lt]
lemma exists_lt_of_prod_lt' [LinearOrder M] [MulRightMono M]
    [MulLeftMono M] {l : List ι} (f g : ι → M)
    (h : (l.map f).prod < (l.map g).prod) : ∃ i ∈ l, f i < g i := by
  contrapose! h
  exact prod_le_prod' h

Existence of Strictly Smaller Element in List Product Inequality

Informal description

Let $M$ be a linearly ordered monoid where multiplication is monotone in both arguments. For any list $l$ of elements in a type $\iota$, and for any two functions $f, g : \iota \to M$, if the product of the mapped values $\prod_{i \in l} f(i)$ is strictly less than the product $\prod_{i \in l} g(i)$, then there exists an element $i \in l$ such that $f(i) < g(i)$.

List.exists_le_of_prod_le' theorem

 [LinearOrder M] [MulLeftStrictMono M] [MulLeftMono M] [MulRightStrictMono M] [MulRightMono M] {l : List ι}
  (hl : l ≠ []) (f g : ι → M) (h : (l.map f).prod ≤ (l.map g).prod) : ∃ x ∈ l, f x ≤ g x

Full source

@[to_additive exists_le_of_sum_le]
lemma exists_le_of_prod_le' [LinearOrder M] [MulLeftStrictMono M]
    [MulLeftMono M] [MulRightStrictMono M]
    [MulRightMono M] {l : List ι} (hl : l ≠ []) (f g : ι → M)
    (h : (l.map f).prod ≤ (l.map g).prod) : ∃ x ∈ l, f x ≤ g x := by
  contrapose! h
  exact prod_lt_prod_of_ne_nil hl _ _ h

Existence of Pointwise Inequality in Non-Empty List Product Comparison

Informal description

Let $M$ be a linearly ordered monoid where multiplication is strictly monotone and monotone in both arguments. For any non-empty list $l$ of elements in a type $\iota$, and for any two functions $f, g : \iota \to M$ such that the product of the mapped values $\prod_{i \in l} f(i) \leq \prod_{i \in l} g(i)$, there exists an element $x \in l$ such that $f(x) \leq g(x)$.

List.one_le_prod_of_one_le theorem

[Preorder M] [MulLeftMono M] {l : List M} (hl₁ : ∀ x ∈ l, (1 : M) ≤ x) : 1 ≤ l.prod

Full source

@[to_additive sum_nonneg]
lemma one_le_prod_of_one_le [Preorder M] [MulLeftMono M] {l : List M}
    (hl₁ : ∀ x ∈ l, (1 : M) ≤ x) : 1 ≤ l.prod := by
  -- We don't use `pow_card_le_prod` to avoid assumption
  -- [covariant_class M M (function.swap (*)) (≤)]
  induction' l with hd tl ih
  · rfl
  rw [prod_cons]
  exact one_le_mul (hl₁ hd mem_cons_self) (ih fun x h => hl₁ x (mem_cons_of_mem hd h))

Product of elements $\geq 1$ in a monoid is $\geq 1$

Informal description

Let $M$ be a preordered monoid with left-monotone multiplication, and let $l$ be a list of elements in $M$. If every element $x$ in $l$ satisfies $1 \leq x$, then the product of all elements in $l$ is greater than or equal to $1$.

List.max_prod_le theorem

 (l : List α) (f g : α → M) [LinearOrder M] [MulLeftMono M] [MulRightMono M] :
  max (l.map f).prod (l.map g).prod ≤ (l.map fun i ↦ max (f i) (g i)).prod

Full source

@[to_additive]
lemma max_prod_le (l : List α) (f g : α → M) [LinearOrder M]
    [MulLeftMono M] [MulRightMono M] :
    max (l.map f).prod (l.map g).prod ≤ (l.map fun i ↦ max (f i) (g i)).prod := by
  rw [max_le_iff]
  constructor <;> apply List.prod_le_prod' <;> intros
  · apply le_max_left
  · apply le_max_right

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

Informal description

Let $M$ be a linearly ordered monoid where multiplication is monotone in both arguments. For any list $l$ of elements in a type $\alpha$, and for any two functions $f, g : \alpha \to M$, the maximum of the products $\max\left(\prod_{i \in l} f(i), \prod_{i \in l} g(i)\right)$ is less than or equal to the product of the pointwise maxima $\prod_{i \in l} \max(f(i), g(i))$.

List.prod_min_le theorem

 [LinearOrder M] [MulLeftMono M] [MulRightMono M] (l : List α) (f g : α → M) :
  (l.map fun i ↦ min (f i) (g i)).prod ≤ min (l.map f).prod (l.map g).prod

Full source

@[to_additive]
lemma prod_min_le [LinearOrder M] [MulLeftMono M]
    [MulRightMono M] (l : List α) (f g : α → M) :
    (l.map fun i ↦ min (f i) (g i)).prod ≤ min (l.map f).prod (l.map g).prod := by
  rw [le_min_iff]
  constructor <;> apply List.prod_le_prod' <;> intros
  · apply min_le_left
  · apply min_le_right

Inequality for Product of Minima in Ordered Monoids: $\prod \min(f,g) \leq \min(\prod f, \prod g)$

Informal description

Let $M$ be a linearly ordered monoid where multiplication is monotone in both arguments. For any list $l$ of elements in a type $\alpha$ and any two functions $f, g : \alpha \to M$, the product of the pointwise minima $\prod_{i \in l} \min(f(i), g(i))$ is less than or equal to the minimum of the products $\min\left(\prod_{i \in l} f(i), \prod_{i \in l} g(i)\right)$.

List.sum_le_foldr_max theorem

 [AddZeroClass M] [Zero N] [LinearOrder N] (f : M → N) (h0 : f 0 ≤ 0) (hadd : ∀ x y, f (x + y) ≤ max (f x) (f y))
  (l : List M) : f l.sum ≤ (l.map f).foldr max 0

Full source

lemma sum_le_foldr_max [AddZeroClass M] [Zero N] [LinearOrder N] (f : M → N) (h0 : f 0 ≤ 0)
    (hadd : ∀ x y, f (x + y) ≤ max (f x) (f y)) (l : List M) : f l.sum ≤ (l.map f).foldr max 0 := by
  induction' l with hd tl IH
  · simpa using h0
  simp only [List.sum_cons, List.foldr_map, List.foldr] at IH ⊢
  exact (hadd _ _).trans (max_le_max le_rfl IH)

Sum Bounded by Maximum under Subadditive Function

Informal description

Let $M$ be an add-zero class and $N$ a linearly ordered type with a zero element. Given a function $f : M \to N$ such that $f(0) \leq 0$ and for all $x, y \in M$, $f(x + y) \leq \max(f(x), f(y))$, then for any list $l$ of elements in $M$, the value of $f$ at the sum of $l$ is bounded above by the maximum value of $f$ over the elements of $l$, i.e., \[ f\left(\sum_{x \in l} x\right) \leq \max_{x \in l} f(x). \]

List.one_lt_prod_of_one_lt theorem

 [CommMonoid M] [PartialOrder M] [IsOrderedMonoid M] : ∀ l : List M, (∀ x ∈ l, (1 : M) < x) → l ≠ [] → 1 < l.prod

Full source

@[to_additive sum_pos]
lemma one_lt_prod_of_one_lt [CommMonoid M] [PartialOrder M] [IsOrderedMonoid M] :
    ∀ l : List M, (∀ x ∈ l, (1 : M) < x) → l ≠ [] → 1 < l.prod
  | [], _, h => (h rfl).elim
  | [b], h, _ => by simpa using h
  | a :: b :: l, hl₁, _ => by
    simp only [forall_eq_or_imp, List.mem_cons] at hl₁
    rw [List.prod_cons]
    apply one_lt_mul_of_lt_of_le' hl₁.1
    apply le_of_lt ((b :: l).one_lt_prod_of_one_lt _ (l.cons_ne_nil b))
    intro x hx; cases hx
    · exact hl₁.2.1
    · exact hl₁.2.2 _ ‹_›

Product of Elements Greater Than One in Ordered Monoid is Greater Than One

Informal description

Let $M$ be a commutative monoid with a partial order such that multiplication is monotone in both arguments. For any nonempty list $l$ of elements in $M$, if every element $x$ in $l$ satisfies $1 < x$, then the product of all elements in $l$ satisfies $1 < \prod l$.

List.single_le_prod theorem

 [CommMonoid M] [PartialOrder M] [IsOrderedMonoid M] {l : List M} (hl₁ : ∀ x ∈ l, (1 : M) ≤ x) : ∀ x ∈ l, x ≤ l.prod

Full source

/-- See also `List.le_prod_of_mem`. -/
@[to_additive "See also `List.le_sum_of_mem`."]
lemma single_le_prod [CommMonoid M] [PartialOrder M] [IsOrderedMonoid M]
    {l : List M} (hl₁ : ∀ x ∈ l, (1 : M) ≤ x) :
    ∀ x ∈ l, x ≤ l.prod := by
  induction l
  · simp
  simp_rw [prod_cons, forall_mem_cons] at hl₁ ⊢
  constructor
  case cons.left => exact le_mul_of_one_le_right' (one_le_prod_of_one_le hl₁.2)
  case cons.right hd tl ih => exact fun x H => le_mul_of_one_le_of_le hl₁.1 (ih hl₁.right x H)

Element-wise Inequality in Ordered Monoid Product

Informal description

Let $M$ be a commutative monoid with a partial order such that multiplication is monotone in both arguments. For any list $l$ of elements in $M$, if every element $x \in l$ satisfies $1 \leq x$, then for every element $x \in l$, we have $x \leq \prod l$.

List.all_one_of_le_one_le_of_prod_eq_one theorem

 [CommMonoid M] [PartialOrder M] [IsOrderedMonoid M] {l : List M} (hl₁ : ∀ x ∈ l, (1 : M) ≤ x) (hl₂ : l.prod = 1)
  {x : M} (hx : x ∈ l) : 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 [CommMonoid M] [PartialOrder M] [IsOrderedMonoid M]
    {l : List M} (hl₁ : ∀ x ∈ l, (1 : M) ≤ x) (hl₂ : l.prod = 1) {x : M} (hx : x ∈ l) : x = 1 :=
  _root_.le_antisymm (hl₂ ▸ single_le_prod hl₁ _ hx) (hl₁ x hx)

All Elements Equal to One When Product is One in Ordered Monoid

Informal description

Let $M$ be an ordered commutative monoid and $l$ be a list of elements in $M$. If every element $x \in l$ satisfies $1 \leq x$ and the product of all elements in $l$ equals $1$, then every element $x \in l$ must be equal to $1$.

List.prod_eq_one_iff theorem

[IsOrderedMonoid M] : l.prod = 1 ↔ ∀ x ∈ l, x = (1 : M)

Full source

@[to_additive] lemma prod_eq_one_iff [IsOrderedMonoid M] : l.prod = 1 ↔ ∀ x ∈ l, x = (1 : M) :=
  ⟨all_one_of_le_one_le_of_prod_eq_one fun _ _ => one_le _, fun h => by
    rw [List.eq_replicate_iff.2 ⟨_, h⟩, prod_replicate, one_pow]
    · exact (length l)
    · rfl⟩

Product Equals One if and only if All Elements are One in Ordered Monoid

Informal description

Let $M$ be an ordered commutative monoid and $l$ be a list of elements in $M$. The product of all elements in $l$ equals $1$ if and only if every element $x \in l$ is equal to $1$.

List.monotone_prod_take theorem

(L : List M) : Monotone fun i => (L.take i).prod

Full source

@[to_additive] lemma monotone_prod_take (L : List M) : Monotone fun i => (L.take i).prod := by
  refine monotone_nat_of_le_succ fun n => ?_
  rcases lt_or_le n L.length with h | h
  · rw [prod_take_succ _ _ h]
    exact le_self_mul
  · simp [take_of_length_le h, take_of_length_le (le_trans h (Nat.le_succ _))]

Monotonicity of Partial Products in Canonically Ordered Monoids

Informal description

For any list $L$ of elements in a canonically ordered multiplicative monoid $M$, the function that takes a natural number $i$ to the product of the first $i$ elements of $L$ is monotone. That is, if $i \leq j$, then $\prod_{k=1}^i L_k \leq \prod_{k=1}^j L_k$.

List.le_prod_of_mem theorem

{xs : List M} {x : M} (h₁ : x ∈ xs) : x ≤ xs.prod

Full source

/-- See also `List.single_le_prod`. -/
@[to_additive "See also `List.single_le_sum`."]
theorem le_prod_of_mem {xs : List M} {x : M} (h₁ : x ∈ xs) : x ≤ xs.prod := by
  induction xs with
  | nil => simp at h₁
  | cons y ys ih =>
    simp only [mem_cons] at h₁
    rcases h₁ with (rfl | h₁)
    · simp
    · specialize ih h₁
      simp only [List.prod_cons]
      exact le_mul_left ih

Element in List is Bounded by Product in Ordered Monoid

Informal description

Let $M$ be a canonically ordered multiplicative monoid, $xs$ be a list of elements in $M$, and $x$ be an element of $M$. If $x$ is a member of the list $xs$, then $x$ is less than or equal to the product of all elements in $xs$.