Documentation

Mathlib.Algebra.Order.BigOperators.Group.List

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₂.sum_le_sum {M : Type u_3} [AddMonoid M] [Preorder M] [CovariantClass M M (Function.swap fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 x2] [CovariantClass M M (fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 x2] {l₁ : List M} {l₂ : List M} (h : List.Forall₂ (fun (x1 x2 : M) => x1 x2) l₁ l₂) :
l₁.sum l₂.sum
theorem List.Forall₂.prod_le_prod' {M : Type u_3} [Monoid M] [Preorder M] [CovariantClass M M (Function.swap fun (x1 x2 : M) => x1 * x2) fun (x1 x2 : M) => x1 x2] [CovariantClass M M (fun (x1 x2 : M) => x1 * x2) fun (x1 x2 : M) => x1 x2] {l₁ : List M} {l₂ : List M} (h : List.Forall₂ (fun (x1 x2 : M) => x1 x2) l₁ l₂) :
l₁.prod l₂.prod
theorem List.Sublist.sum_le_sum {M : Type u_3} [AddMonoid M] [Preorder M] [CovariantClass M M (Function.swap fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 x2] [CovariantClass M M (fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 x2] {l₁ : List M} {l₂ : List M} (h : l₁.Sublist l₂) (h₁ : al₂, 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.Sublist.prod_le_prod' {M : Type u_3} [Monoid M] [Preorder M] [CovariantClass M M (Function.swap fun (x1 x2 : M) => x1 * x2) fun (x1 x2 : M) => x1 x2] [CovariantClass M M (fun (x1 x2 : M) => x1 * x2) fun (x1 x2 : M) => x1 x2] {l₁ : List M} {l₂ : List M} (h : l₁.Sublist l₂) (h₁ : al₂, 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.SublistForall₂.sum_le_sum {M : Type u_3} [AddMonoid M] [Preorder M] [CovariantClass M M (Function.swap fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 x2] [CovariantClass M M (fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 x2] {l₁ : List M} {l₂ : List M} (h : List.SublistForall₂ (fun (x1 x2 : M) => x1 x2) l₁ l₂) (h₁ : al₂, 0 a) :
l₁.sum l₂.sum
theorem List.SublistForall₂.prod_le_prod' {M : Type u_3} [Monoid M] [Preorder M] [CovariantClass M M (Function.swap fun (x1 x2 : M) => x1 * x2) fun (x1 x2 : M) => x1 x2] [CovariantClass M M (fun (x1 x2 : M) => x1 * x2) fun (x1 x2 : M) => x1 x2] {l₁ : List M} {l₂ : List M} (h : List.SublistForall₂ (fun (x1 x2 : M) => x1 x2) l₁ l₂) (h₁ : al₂, 1 a) :
l₁.prod l₂.prod
theorem List.sum_le_sum {ι : Type u_1} {M : Type u_3} [AddMonoid M] [Preorder M] [CovariantClass M M (Function.swap fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 x2] [CovariantClass M M (fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 x2] {l : List ι} {f : ιM} {g : ιM} (h : il, f i g i) :
(List.map f l).sum (List.map g l).sum
theorem List.prod_le_prod' {ι : Type u_1} {M : Type u_3} [Monoid M] [Preorder M] [CovariantClass M M (Function.swap fun (x1 x2 : M) => x1 * x2) fun (x1 x2 : M) => x1 x2] [CovariantClass M M (fun (x1 x2 : M) => x1 * x2) fun (x1 x2 : M) => x1 x2] {l : List ι} {f : ιM} {g : ιM} (h : il, f i g i) :
(List.map f l).prod (List.map g l).prod
theorem List.sum_lt_sum {ι : Type u_1} {M : Type u_3} [AddMonoid M] [Preorder M] [CovariantClass M M (fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 < x2] [CovariantClass M M (fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 x2] [CovariantClass M M (Function.swap fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 < x2] [CovariantClass M M (Function.swap fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 x2] {l : List ι} (f : ιM) (g : ιM) (h₁ : il, f i g i) (h₂ : il, f i < g i) :
(List.map f l).sum < (List.map g l).sum
theorem List.prod_lt_prod' {ι : Type u_1} {M : Type u_3} [Monoid M] [Preorder M] [CovariantClass M M (fun (x1 x2 : M) => x1 * x2) fun (x1 x2 : M) => x1 < x2] [CovariantClass M M (fun (x1 x2 : M) => x1 * x2) fun (x1 x2 : M) => x1 x2] [CovariantClass M M (Function.swap fun (x1 x2 : M) => x1 * x2) fun (x1 x2 : M) => x1 < x2] [CovariantClass M M (Function.swap fun (x1 x2 : M) => x1 * x2) fun (x1 x2 : M) => x1 x2] {l : List ι} (f : ιM) (g : ιM) (h₁ : il, f i g i) (h₂ : il, f i < g i) :
(List.map f l).prod < (List.map g l).prod
theorem List.sum_lt_sum_of_ne_nil {ι : Type u_1} {M : Type u_3} [AddMonoid M] [Preorder M] [CovariantClass M M (fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 < x2] [CovariantClass M M (fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 x2] [CovariantClass M M (Function.swap fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 < x2] [CovariantClass M M (Function.swap fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 x2] {l : List ι} (hl : l []) (f : ιM) (g : ιM) (hlt : il, f i < g i) :
(List.map f l).sum < (List.map g l).sum
theorem List.prod_lt_prod_of_ne_nil {ι : Type u_1} {M : Type u_3} [Monoid M] [Preorder M] [CovariantClass M M (fun (x1 x2 : M) => x1 * x2) fun (x1 x2 : M) => x1 < x2] [CovariantClass M M (fun (x1 x2 : M) => x1 * x2) fun (x1 x2 : M) => x1 x2] [CovariantClass M M (Function.swap fun (x1 x2 : M) => x1 * x2) fun (x1 x2 : M) => x1 < x2] [CovariantClass M M (Function.swap fun (x1 x2 : M) => x1 * x2) fun (x1 x2 : M) => x1 x2] {l : List ι} (hl : l []) (f : ιM) (g : ιM) (hlt : il, f i < g i) :
(List.map f l).prod < (List.map g l).prod
theorem List.sum_le_card_nsmul {M : Type u_3} [AddMonoid M] [Preorder M] [CovariantClass M M (Function.swap fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 x2] [CovariantClass M M (fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 x2] (l : List M) (n : M) (h : xl, x n) :
l.sum l.length n
theorem List.prod_le_pow_card {M : Type u_3} [Monoid M] [Preorder M] [CovariantClass M M (Function.swap fun (x1 x2 : M) => x1 * x2) fun (x1 x2 : M) => x1 x2] [CovariantClass M M (fun (x1 x2 : M) => x1 * x2) fun (x1 x2 : M) => x1 x2] (l : List M) (n : M) (h : xl, x n) :
l.prod n ^ l.length
theorem List.card_nsmul_le_sum {M : Type u_3} [AddMonoid M] [Preorder M] [CovariantClass M M (Function.swap fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 x2] [CovariantClass M M (fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 x2] (l : List M) (n : M) (h : xl, n x) :
l.length n l.sum
theorem List.pow_card_le_prod {M : Type u_3} [Monoid M] [Preorder M] [CovariantClass M M (Function.swap fun (x1 x2 : M) => x1 * x2) fun (x1 x2 : M) => x1 x2] [CovariantClass M M (fun (x1 x2 : M) => x1 * x2) fun (x1 x2 : M) => x1 x2] (l : List M) (n : M) (h : xl, n x) :
n ^ l.length l.prod
theorem List.exists_lt_of_sum_lt {ι : Type u_1} {M : Type u_3} [AddMonoid M] [LinearOrder M] [CovariantClass M M (Function.swap fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 x2] [CovariantClass M M (fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 x2] {l : List ι} (f : ιM) (g : ιM) (h : (List.map f l).sum < (List.map g l).sum) :
il, f i < g i
theorem List.exists_lt_of_prod_lt' {ι : Type u_1} {M : Type u_3} [Monoid M] [LinearOrder M] [CovariantClass M M (Function.swap fun (x1 x2 : M) => x1 * x2) fun (x1 x2 : M) => x1 x2] [CovariantClass M M (fun (x1 x2 : M) => x1 * x2) fun (x1 x2 : M) => x1 x2] {l : List ι} (f : ιM) (g : ιM) (h : (List.map f l).prod < (List.map g l).prod) :
il, f i < g i
theorem List.exists_le_of_sum_le {ι : Type u_1} {M : Type u_3} [AddMonoid M] [LinearOrder M] [CovariantClass M M (fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 < x2] [CovariantClass M M (fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 x2] [CovariantClass M M (Function.swap fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 < x2] [CovariantClass M M (Function.swap fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 x2] {l : List ι} (hl : l []) (f : ιM) (g : ιM) (h : (List.map f l).sum (List.map g l).sum) :
xl, f x g x
theorem List.exists_le_of_prod_le' {ι : Type u_1} {M : Type u_3} [Monoid M] [LinearOrder M] [CovariantClass M M (fun (x1 x2 : M) => x1 * x2) fun (x1 x2 : M) => x1 < x2] [CovariantClass M M (fun (x1 x2 : M) => x1 * x2) fun (x1 x2 : M) => x1 x2] [CovariantClass M M (Function.swap fun (x1 x2 : M) => x1 * x2) fun (x1 x2 : M) => x1 < x2] [CovariantClass M M (Function.swap fun (x1 x2 : M) => x1 * x2) fun (x1 x2 : M) => x1 x2] {l : List ι} (hl : l []) (f : ιM) (g : ιM) (h : (List.map f l).prod (List.map g l).prod) :
xl, f x g x
theorem List.sum_nonneg {M : Type u_3} [AddMonoid M] [Preorder M] [CovariantClass M M (fun (x1 x2 : M) => x1 + x2) fun (x1 x2 : M) => x1 x2] {l : List M} (hl₁ : xl, 0 x) :
0 l.sum
theorem List.one_le_prod_of_one_le {M : Type u_3} [Monoid M] [Preorder M] [CovariantClass M M (fun (x1 x2 : M) => x1 * x2) fun (x1 x2 : M) => x1 x2] {l : List M} (hl₁ : xl, 1 x) :
1 l.prod
theorem List.sum_le_foldr_max {M : Type u_3} {N : Type u_4} [AddMonoid M] [AddMonoid N] [LinearOrder N] (f : MN) (h0 : f 0 0) (hadd : ∀ (x y : M), f (x + y) max (f x) (f y)) (l : List M) :
f l.sum List.foldr max 0 (List.map f l)
theorem List.sum_pos {M : Type u_3} [OrderedAddCommMonoid M] (l : List M) :
(∀ xl, 0 < x)l []0 < l.sum
theorem List.one_lt_prod_of_one_lt {M : Type u_3} [OrderedCommMonoid M] (l : List M) :
(∀ xl, 1 < x)l []1 < l.prod
theorem List.single_le_sum {M : Type u_3} [OrderedAddCommMonoid M] {l : List M} (hl₁ : xl, 0 x) (x : M) :
x lx l.sum

See also List.le_sum_of_mem.

theorem List.single_le_prod {M : Type u_3} [OrderedCommMonoid M] {l : List M} (hl₁ : xl, 1 x) (x : M) :
x lx l.prod

See also List.le_prod_of_mem.

theorem List.all_zero_of_le_zero_le_of_sum_eq_zero {M : Type u_3} [OrderedAddCommMonoid M] {l : List M} (hl₁ : xl, 0 x) (hl₂ : l.sum = 0) {x : M} (hx : x l) :
x = 0
theorem List.all_one_of_le_one_le_of_prod_eq_one {M : Type u_3} [OrderedCommMonoid M] {l : List M} (hl₁ : xl, 1 x) (hl₂ : l.prod = 1) {x : M} (hx : x l) :
x = 1
theorem List.sum_eq_zero_iff {M : Type u_3} [CanonicallyOrderedAddCommMonoid M] {l : List M} :
l.sum = 0 xl, x = 0
theorem List.prod_eq_one_iff {M : Type u_3} [CanonicallyOrderedCommMonoid M] {l : List M} :
l.prod = 1 xl, x = 1
theorem List.monotone_sum_take {M : Type u_3} [CanonicallyOrderedAddCommMonoid M] (L : List M) :
Monotone fun (i : ) => (List.take i L).sum
theorem List.monotone_prod_take {M : Type u_3} [CanonicallyOrderedCommMonoid M] (L : List M) :
Monotone fun (i : ) => (List.take i L).prod
theorem List.le_sum_of_mem {M : Type u_3} [CanonicallyOrderedAddCommMonoid M] {xs : List M} {x : M} (h₁ : x xs) :
x xs.sum

See also List.single_le_sum.

theorem List.le_prod_of_mem {M : Type u_3} [CanonicallyOrderedCommMonoid M] {xs : List M} {x : M} (h₁ : x xs) :
x xs.prod

See also List.single_le_prod.