Big operators on a list in ordered groups

This file contains the results concerning the interaction of list big operators with ordered groups/monoids.

theorem List.Forall₂.prod_le_prod' {M : Type u_3} [Monoid M] [Preorder M] [MulRightMono M] [MulLeftMono M] {l₁ l₂ : List M} (h : Forall₂ (fun (x1 x2 : M) => x1 ≤ x2) l₁ l₂) : l₁.prod ≤ l₂.prod

theorem List.Forall₂.sum_le_sum {M : Type u_3} [AddMonoid M] [Preorder M] [AddRightMono M] [AddLeftMono M] {l₁ l₂ : List M} (h : Forall₂ (fun (x1 x2 : M) => x1 ≤ x2) l₁ l₂) : l₁.sum ≤ l₂.sum

theorem List.Sublist.prod_le_prod' {M : Type u_3} [Monoid M] [Preorder M] [MulRightMono M] [MulLeftMono M] {l₁ l₂ : List M} (h : l₁.Sublist l₂) (h₁ : ∀ (a : M), a ∈ l₂ → 1 ≤ a) : l₁.prod ≤ l₂.prod

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.

theorem List.Sublist.sum_le_sum {M : Type u_3} [AddMonoid M] [Preorder M] [AddRightMono M] [AddLeftMono M] {l₁ l₂ : List M} (h : l₁.Sublist l₂) (h₁ : ∀ (a : M), a ∈ l₂ → 0 ≤ a) : l₁.sum ≤ l₂.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.

theorem List.SublistForall₂.prod_le_prod' {M : Type u_3} [Monoid M] [Preorder M] [MulRightMono M] [MulLeftMono M] {l₁ l₂ : List M} (h : SublistForall₂ (fun (x1 x2 : M) => x1 ≤ x2) l₁ l₂) (h₁ : ∀ (a : M), a ∈ l₂ → 1 ≤ a) : l₁.prod ≤ l₂.prod

theorem List.SublistForall₂.sum_le_sum {M : Type u_3} [AddMonoid M] [Preorder M] [AddRightMono M] [AddLeftMono M] {l₁ l₂ : List M} (h : SublistForall₂ (fun (x1 x2 : M) => x1 ≤ x2) l₁ l₂) (h₁ : ∀ (a : M), a ∈ l₂ → 0 ≤ a) : l₁.sum ≤ l₂.sum

theorem List.prod_le_prod' {ι : Type u_1} {M : Type u_3} [Monoid M] [Preorder M] [MulRightMono M] [MulLeftMono M] {l : List ι} {f g : ι → M} (h : ∀ (i : ι), i ∈ l → f i ≤ g i) : (map f l).prod ≤ (map g l).prod

theorem List.sum_le_sum {ι : Type u_1} {M : Type u_3} [AddMonoid M] [Preorder M] [AddRightMono M] [AddLeftMono M] {l : List ι} {f g : ι → M} (h : ∀ (i : ι), i ∈ l → f i ≤ g i) : (map f l).sum ≤ (map g l).sum

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

theorem List.sum_lt_sum {ι : Type u_1} {M : Type u_3} [AddMonoid M] [Preorder M] [AddLeftStrictMono M] [AddLeftMono M] [AddRightStrictMono M] [AddRightMono M] {l : List ι} (f g : ι → M) (h₁ : ∀ (i : ι), i ∈ l → f i ≤ g i) (h₂ : ∃ (i : ι), i ∈ l ∧ f i < g i) : (map f l).sum < (map g l).sum

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

theorem List.sum_lt_sum_of_ne_nil {ι : Type u_1} {M : Type u_3} [AddMonoid M] [Preorder M] [AddLeftStrictMono M] [AddLeftMono M] [AddRightStrictMono M] [AddRightMono M] {l : List ι} (hl : l ≠ []) (f g : ι → M) (hlt : ∀ (i : ι), i ∈ l → f i < g i) : (map f l).sum < (map g l).sum

theorem List.prod_le_pow_length {M : Type u_3} [Monoid M] [Preorder M] [MulRightMono M] [MulLeftMono M] (l : List M) (n : M) (h : ∀ (x : M), x ∈ l → x ≤ n) : l.prod ≤ n ^ l.length

theorem List.sum_le_length_nsmul {M : Type u_3} [AddMonoid M] [Preorder M] [AddRightMono M] [AddLeftMono M] (l : List M) (n : M) (h : ∀ (x : M), x ∈ l → x ≤ n) : l.sum ≤ l.length • n

@[deprecated List.prod_le_pow_length (since := "2026-08-26")]

theorem List.prod_le_pow_card {M : Type u_3} [Monoid M] [Preorder M] [MulRightMono M] [MulLeftMono M] (l : List M) (n : M) (h : ∀ (x : M), x ∈ l → x ≤ n) : l.prod ≤ n ^ l.length

Alias of List.prod_le_pow_length.

@[deprecated List.sum_le_length_nsmul (since := "2026-08-26")]

theorem List.sum_le_card_nsmul {M : Type u_3} [AddMonoid M] [Preorder M] [AddRightMono M] [AddLeftMono M] (l : List M) (n : M) (h : ∀ (x : M), x ∈ l → x ≤ n) : l.sum ≤ l.length • n

Alias of List.sum_le_length_nsmul.

theorem List.pow_length_le_prod {M : Type u_3} [Monoid M] [Preorder M] [MulRightMono M] [MulLeftMono M] (l : List M) (n : M) (h : ∀ (x : M), x ∈ l → n ≤ x) : n ^ l.length ≤ l.prod

theorem List.length_nsmul_le_sum {M : Type u_3} [AddMonoid M] [Preorder M] [AddRightMono M] [AddLeftMono M] (l : List M) (n : M) (h : ∀ (x : M), x ∈ l → n ≤ x) : l.length • n ≤ l.sum

@[deprecated List.pow_length_le_prod (since := "2026-08-26")]

theorem List.pow_card_le_prod {M : Type u_3} [Monoid M] [Preorder M] [MulRightMono M] [MulLeftMono M] (l : List M) (n : M) (h : ∀ (x : M), x ∈ l → n ≤ x) : n ^ l.length ≤ l.prod

Alias of List.pow_length_le_prod.

@[deprecated List.length_nsmul_le_sum (since := "2026-08-26")]

theorem List.card_nsmul_le_sum {M : Type u_3} [AddMonoid M] [Preorder M] [AddRightMono M] [AddLeftMono M] (l : List M) (n : M) (h : ∀ (x : M), x ∈ l → n ≤ x) : l.length • n ≤ l.sum

Alias of List.length_nsmul_le_sum.

theorem List.exists_lt_of_prod_lt' {ι : Type u_1} {M : Type u_3} [Monoid M] [LinearOrder M] [MulRightMono M] [MulLeftMono M] {l : List ι} (f g : ι → M) (h : (map f l).prod < (map g l).prod) : ∃ (i : ι), i ∈ l ∧ f i < g i

theorem List.exists_lt_of_sum_lt {ι : Type u_1} {M : Type u_3} [AddMonoid M] [LinearOrder M] [AddRightMono M] [AddLeftMono M] {l : List ι} (f g : ι → M) (h : (map f l).sum < (map g l).sum) : ∃ (i : ι), i ∈ l ∧ f i < g i

theorem List.exists_le_of_prod_le' {ι : Type u_1} {M : Type u_3} [Monoid M] [LinearOrder M] [MulLeftStrictMono M] [MulLeftMono M] [MulRightStrictMono M] [MulRightMono M] {l : List ι} (hl : l ≠ []) (f g : ι → M) (h : (map f l).prod ≤ (map g l).prod) : ∃ (x : ι), x ∈ l ∧ f x ≤ g x

theorem List.exists_le_of_sum_le {ι : Type u_1} {M : Type u_3} [AddMonoid M] [LinearOrder M] [AddLeftStrictMono M] [AddLeftMono M] [AddRightStrictMono M] [AddRightMono M] {l : List ι} (hl : l ≠ []) (f g : ι → M) (h : (map f l).sum ≤ (map g l).sum) : ∃ (x : ι), x ∈ l ∧ f x ≤ g x

theorem List.one_le_prod_of_one_le {M : Type u_3} [Monoid M] [Preorder M] [MulLeftMono M] {l : List M} (hl₁ : ∀ (x : M), x ∈ l → 1 ≤ x) : 1 ≤ l.prod

theorem List.sum_nonneg {M : Type u_3} [AddMonoid M] [Preorder M] [AddLeftMono M] {l : List M} (hl₁ : ∀ (x : M), x ∈ l → 0 ≤ x) : 0 ≤ l.sum

theorem List.max_prod_le {α : Type u_2} {M : Type u_3} [Monoid M] (l : List α) (f g : α → M) [LinearOrder M] [MulLeftMono M] [MulRightMono M] : max (map f l).prod (map g l).prod ≤ (map (fun (i : α) => max (f i) (g i)) l).prod

theorem List.max_sum_le {α : Type u_2} {M : Type u_3} [AddMonoid M] (l : List α) (f g : α → M) [LinearOrder M] [AddLeftMono M] [AddRightMono M] : max (map f l).sum (map g l).sum ≤ (map (fun (i : α) => max (f i) (g i)) l).sum

theorem List.prod_min_le {α : Type u_2} {M : Type u_3} [Monoid M] [LinearOrder M] [MulLeftMono M] [MulRightMono M] (l : List α) (f g : α → M) : (map (fun (i : α) => min (f i) (g i)) l).prod ≤ min (map f l).prod (map g l).prod

theorem List.sum_min_le {α : Type u_2} {M : Type u_3} [AddMonoid M] [LinearOrder M] [AddLeftMono M] [AddRightMono M] (l : List α) (f g : α → M) : (map (fun (i : α) => min (f i) (g i)) l).sum ≤ min (map f l).sum (map g l).sum

theorem List.monotone_prod_take {M : Type u_3} [Monoid M] [Preorder M] [CanonicallyOrderedMul M] (L : List M) : Monotone fun (i : ℕ) => (take i L).prod

theorem List.monotone_sum_take {M : Type u_3} [AddMonoid M] [Preorder M] [CanonicallyOrderedAdd M] (L : List M) : Monotone fun (i : ℕ) => (take i L).sum

theorem List.le_prod_of_mem {M : Type u_3} [Monoid M] [Preorder M] [CanonicallyOrderedMul M] {xs : List M} {x : M} (h₁ : x ∈ xs) : x ≤ xs.prod

See also List.single_le_prod.

theorem List.le_sum_of_mem {M : Type u_3} [AddMonoid M] [Preorder M] [CanonicallyOrderedAdd M] {xs : List M} {x : M} (h₁ : x ∈ xs) : x ≤ xs.sum

See also List.single_le_sum.

theorem List.le_prod_of_submultiplicative_on_pred {α : Type u_5} {β : Type u_6} [Monoid α] [CommMonoid β] [Preorder β] [IsOrderedMonoid β] (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)) (l : List α) (hpl : ∀ (a : α), a ∈ l → p a) : f l.prod ≤ (map f l).prod

theorem List.le_sum_of_subadditive_on_pred {α : Type u_5} {β : Type u_6} [AddMonoid α] [AddCommMonoid β] [Preorder β] [IsOrderedAddMonoid β] (f : α → β) (p : α → Prop) (h_zero : f 0 ≤ 0) (hp_zero : p 0) (h_add : ∀ (a b : α), p a → p b → f (a + b) ≤ f a + f b) (hp_add : ∀ (a b : α), p a → p b → p (a + b)) (l : List α) (hpl : ∀ (a : α), a ∈ l → p a) : f l.sum ≤ (map f l).sum

theorem List.le_prod_of_submultiplicative {α : Type u_5} {β : Type u_6} [Monoid α] [CommMonoid β] [Preorder β] [IsOrderedMonoid β] (f : α → β) (h_one : f 1 ≤ 1) (h_mul : ∀ (a b : α), f (a * b) ≤ f a * f b) (l : List α) : f l.prod ≤ (map f l).prod

theorem List.le_sum_of_subadditive {α : Type u_5} {β : Type u_6} [AddMonoid α] [AddCommMonoid β] [Preorder β] [IsOrderedAddMonoid β] (f : α → β) (h_zero : f 0 ≤ 0) (h_add : ∀ (a b : α), f (a + b) ≤ f a + f b) (l : List α) : f l.sum ≤ (map f l).sum

theorem List.le_prod_nonempty_of_submultiplicative_on_pred {α : Type u_5} {β : Type u_6} [Monoid α] [CommMonoid β] [Preorder β] [IsOrderedMonoid β] (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)) (l : List α) (hl_nonempty : l ≠ []) (hl : ∀ (a : α), a ∈ l → p a) : f l.prod ≤ (map f l).prod

theorem List.le_sum_nonempty_of_subadditive_on_pred {α : Type u_5} {β : Type u_6} [AddMonoid α] [AddCommMonoid β] [Preorder β] [IsOrderedAddMonoid β] (f : α → β) (p : α → Prop) (h_add : ∀ (a b : α), p a → p b → f (a + b) ≤ f a + f b) (hp_add : ∀ (a b : α), p a → p b → p (a + b)) (l : List α) (hl_nonempty : l ≠ []) (hl : ∀ (a : α), a ∈ l → p a) : f l.sum ≤ (map f l).sum

theorem List.le_prod_nonempty_of_submultiplicative {α : Type u_5} {β : Type u_6} [Monoid α] [CommMonoid β] [Preorder β] [IsOrderedMonoid β] (f : α → β) (h_mul : ∀ (a b : α), f (a * b) ≤ f a * f b) (l : List α) (hs_nonempty : l ≠ ∅) : f l.prod ≤ (map f l).prod

theorem List.le_sum_nonempty_of_subadditive {α : Type u_5} {β : Type u_6} [AddMonoid α] [AddCommMonoid β] [Preorder β] [IsOrderedAddMonoid β] (f : α → β) (h_add : ∀ (a b : α), f (a + b) ≤ f a + f b) (l : List α) (hs_nonempty : l ≠ ∅) : f l.sum ≤ (map f l).sum

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

theorem List.one_lt_prod_of_one_lt {M : Type u_3} [CommMonoid M] [Preorder M] [IsOrderedMonoid M] (l : List M) : (∀ (x : M), x ∈ l → 1 < x) → l ≠ [] → 1 < l.prod

theorem List.sum_pos {M : Type u_3} [AddCommMonoid M] [Preorder M] [IsOrderedAddMonoid M] (l : List M) : (∀ (x : M), x ∈ l → 0 < x) → l ≠ [] → 0 < l.sum

theorem List.single_le_prod {M : Type u_3} [CommMonoid M] [Preorder M] [IsOrderedMonoid M] {l : List M} (hl₁ : ∀ (x : M), x ∈ l → 1 ≤ x) (x : M) : x ∈ l → x ≤ l.prod

See also List.le_prod_of_mem.

theorem List.single_le_sum {M : Type u_3} [AddCommMonoid M] [Preorder M] [IsOrderedAddMonoid M] {l : List M} (hl₁ : ∀ (x : M), x ∈ l → 0 ≤ x) (x : M) : x ∈ l → x ≤ l.sum

See also List.le_sum_of_mem.

theorem List.all_one_of_le_one_le_of_prod_eq_one {M : Type u_3} [CommMonoid M] [PartialOrder M] [IsOrderedMonoid M] {l : List M} (hl₁ : ∀ (x : M), x ∈ l → 1 ≤ x) (hl₂ : l.prod = 1) {x : M} (hx : x ∈ l) : x = 1

theorem List.all_zero_of_le_zero_le_of_sum_eq_zero {M : Type u_3} [AddCommMonoid M] [PartialOrder M] [IsOrderedAddMonoid M] {l : List M} (hl₁ : ∀ (x : M), x ∈ l → 0 ≤ x) (hl₂ : l.sum = 0) {x : M} (hx : x ∈ l) : x = 0

theorem List.prod_eq_one_iff {M : Type u_3} [CommMonoid M] [PartialOrder M] [IsOrderedMonoid M] [CanonicallyOrderedMul M] {l : List M} : l.prod = 1 ↔ ∀ (x : M), x ∈ l → x = 1

theorem List.sum_eq_zero_iff {M : Type u_3} [AddCommMonoid M] [PartialOrder M] [IsOrderedAddMonoid M] [CanonicallyOrderedAdd M] {l : List M} : l.sum = 0 ↔ ∀ (x : M), x ∈ l → x = 0

theorem List.apply_prod_le_sum_map {α : Type u_5} {β : Type u_6} [Monoid α] [AddMonoid β] [Preorder β] [AddLeftMono β] (l : List α) (f : α → β) (h_one : f 1 ≤ 0) (h_mul : ∀ (a b : α), f (a * b) ≤ f a + f b) : f l.prod ≤ (map f l).sum

theorem List.sum_map_le_apply_prod {α : Type u_5} {β : Type u_6} [Monoid α] [AddMonoid β] [Preorder β] [AddLeftMono β] (l : List α) (f : α → β) (h_one : 0 ≤ f 1) (h_mul : ∀ (a b : α), f a + f b ≤ f (a * b)) : (map f l).sum ≤ f l.prod