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 (x x_1 : M) => x + x_1) fun (x x_1 : M) => x ≤ x_1]
[CovariantClass M M (fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x ≤ x_1]
{l₁ : List M}
{l₂ : List M}
(h : List.Forall₂ (fun (x x_1 : M) => x ≤ x_1) 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 (x x_1 : M) => x * x_1) fun (x x_1 : M) => x ≤ x_1]
[CovariantClass M M (fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x ≤ x_1]
{l₁ : List M}
{l₂ : List M}
(h : List.Forall₂ (fun (x x_1 : M) => x ≤ x_1) 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 (x x_1 : M) => x + x_1) fun (x x_1 : M) => x ≤ x_1]
[CovariantClass M M (fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x ≤ x_1]
{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 (x x_1 : M) => x * x_1) fun (x x_1 : M) => x ≤ x_1]
[CovariantClass M M (fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x ≤ x_1]
{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
.
abbrev
List.SublistForall₂.sum_le_sum.match_1
{M : Type u_1}
[Preorder M]
{l₁ : List M}
{l₂ : List M}
(motive : (∃ (l : List M), List.Forall₂ (fun (x x_1 : M) => x ≤ x_1) l₁ l ∧ l.Sublist l₂) → Prop)
:
∀ (x : ∃ (l : List M), List.Forall₂ (fun (x x_1 : M) => x ≤ x_1) l₁ l ∧ l.Sublist l₂),
(∀ (w : List M) (hall : List.Forall₂ (fun (x x_1 : M) => x ≤ x_1) l₁ w) (hsub : w.Sublist l₂), motive ⋯) → motive x
Equations
- ⋯ = ⋯
Instances For
theorem
List.SublistForall₂.sum_le_sum
{M : Type u_3}
[AddMonoid M]
[Preorder M]
[CovariantClass M M (Function.swap fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x ≤ x_1]
[CovariantClass M M (fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x ≤ x_1]
{l₁ : List M}
{l₂ : List M}
(h : List.SublistForall₂ (fun (x x_1 : M) => x ≤ x_1) 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 (x x_1 : M) => x * x_1) fun (x x_1 : M) => x ≤ x_1]
[CovariantClass M M (fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x ≤ x_1]
{l₁ : List M}
{l₂ : List M}
(h : List.SublistForall₂ (fun (x x_1 : M) => x ≤ x_1) 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 (x x_1 : M) => x + x_1) fun (x x_1 : M) => x ≤ x_1]
[CovariantClass M M (fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x ≤ x_1]
{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 (x x_1 : M) => x * x_1) fun (x x_1 : M) => x ≤ x_1]
[CovariantClass M M (fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x ≤ x_1]
{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 (x x_1 : M) => x + x_1) fun (x x_1 : M) => x < x_1]
[CovariantClass M M (fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x ≤ x_1]
[CovariantClass M M (Function.swap fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x < x_1]
[CovariantClass M M (Function.swap fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x ≤ x_1]
{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 (x x_1 : M) => x * x_1) fun (x x_1 : M) => x < x_1]
[CovariantClass M M (fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x ≤ x_1]
[CovariantClass M M (Function.swap fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x < x_1]
[CovariantClass M M (Function.swap fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x ≤ x_1]
{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 (x x_1 : M) => x + x_1) fun (x x_1 : M) => x < x_1]
[CovariantClass M M (fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x ≤ x_1]
[CovariantClass M M (Function.swap fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x < x_1]
[CovariantClass M M (Function.swap fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x ≤ x_1]
{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 (x x_1 : M) => x * x_1) fun (x x_1 : M) => x < x_1]
[CovariantClass M M (fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x ≤ x_1]
[CovariantClass M M (Function.swap fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x < x_1]
[CovariantClass M M (Function.swap fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x ≤ x_1]
{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 (x x_1 : M) => x + x_1) fun (x x_1 : M) => x ≤ x_1]
[CovariantClass M M (fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x ≤ x_1]
(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 (x x_1 : M) => x * x_1) fun (x x_1 : M) => x ≤ x_1]
[CovariantClass M M (fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x ≤ x_1]
(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 (x x_1 : M) => x + x_1) fun (x x_1 : M) => x ≤ x_1]
[CovariantClass M M (fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x ≤ x_1]
(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 (x x_1 : M) => x * x_1) fun (x x_1 : M) => x ≤ x_1]
[CovariantClass M M (fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x ≤ x_1]
(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 (x x_1 : M) => x + x_1) fun (x x_1 : M) => x ≤ x_1]
[CovariantClass M M (fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x ≤ x_1]
{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 (x x_1 : M) => x * x_1) fun (x x_1 : M) => x ≤ x_1]
[CovariantClass M M (fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x ≤ x_1]
{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 (x x_1 : M) => x + x_1) fun (x x_1 : M) => x < x_1]
[CovariantClass M M (fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x ≤ x_1]
[CovariantClass M M (Function.swap fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x < x_1]
[CovariantClass M M (Function.swap fun (x x_1 : M) => x + x_1) fun (x x_1 : M) => x ≤ x_1]
{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 (x x_1 : M) => x * x_1) fun (x x_1 : M) => x < x_1]
[CovariantClass M M (fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x ≤ x_1]
[CovariantClass M M (Function.swap fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x < x_1]
[CovariantClass M M (Function.swap fun (x x_1 : M) => x * x_1) fun (x x_1 : M) => x ≤ x_1]
{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)
abbrev
List.sum_pos.match_1
{M : Type u_1}
[OrderedAddCommMonoid M]
(motive : (x : List M) → (∀ x_1 ∈ x, 0 < x_1) → x ≠ [] → Prop)
:
∀ (x : List M) (x_1 : ∀ x_1 ∈ x, 0 < x_1) (x_2 : x ≠ []),
(∀ (x : ∀ x ∈ [], 0 < x) (h : [] ≠ []), motive [] x h) →
(∀ (b : M) (h : ∀ x ∈ [b], 0 < x) (x : [b] ≠ []), motive [b] h x) →
(∀ (a b : M) (l : List M) (hl₁ : ∀ x ∈ a :: b :: l, 0 < x) (x : a :: b :: l ≠ []), motive (a :: b :: l) hl₁ x) →
motive x x_1 x_2
Equations
- ⋯ = ⋯
Instances For
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