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₁ : ∀ 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.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₁ : ∀ 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.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₁ : ∀ a ∈ l₂, 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₁ : ∀ a ∈ l₂, 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 : ∀ i ∈ l, f i ≤ g i)
:
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 : ∀ i ∈ l, f i ≤ g i)
:
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₁ : ∀ i ∈ l, f i ≤ g i)
(h₂ : ∃ i ∈ l, f i < g i)
:
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₁ : ∀ i ∈ l, f i ≤ g i)
(h₂ : ∃ i ∈ l, f i < g i)
:
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 : ∀ i ∈ l, f i < g i)
:
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 : ∀ i ∈ l, f i < g i)
:
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 : ∀ x ∈ l, x ≤ 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 : ∀ x ∈ l, x ≤ n)
:
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 : ∀ x ∈ l, n ≤ x)
:
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 : ∀ x ∈ l, n ≤ x)
:
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)
:
∃ i ∈ l, 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)
:
∃ i ∈ l, 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)
:
∃ x ∈ l, 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)
:
∃ x ∈ l, f x ≤ g x
theorem
List.sum_le_foldr_max
{M : Type u_3}
{N : Type u_4}
[AddMonoid M]
[AddMonoid 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 ≤ List.foldr max 0 (List.map f l)
theorem
List.single_le_sum
{M : Type u_3}
[OrderedAddCommMonoid M]
{l : List M}
(hl₁ : ∀ x ∈ l, 0 ≤ x)
(x : M)
:
theorem
List.single_le_prod
{M : Type u_3}
[OrderedCommMonoid M]
{l : List M}
(hl₁ : ∀ x ∈ l, 1 ≤ x)
(x : M)
:
theorem
List.all_zero_of_le_zero_le_of_sum_eq_zero
{M : Type u_3}
[OrderedAddCommMonoid M]
{l : List M}
(hl₁ : ∀ x ∈ l, 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₁ : ∀ x ∈ l, 1 ≤ x)
(hl₂ : l.prod = 1)
{x : M}
(hx : x ∈ l)
:
x = 1