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

• ⋯ = ⋯

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) : (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 (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) : (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 (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) : (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 (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) : (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 (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) : (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 (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) : (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 (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) : 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 (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) : 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 (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) : 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 (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) : 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 (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_nonneg {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] {l : List M} (hl₁ : ∀ x ∈ l, 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 (x x_1 : M) => x * x_1) fun (x x_1 : M) => x ≤ x_1] {l : List M} (hl₁ : ∀ x ∈ l, 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 : 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

• ⋯ = ⋯

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

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

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

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

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

theorem List.sum_eq_zero_iff {M : Type u_3} [CanonicallyOrderedAddCommMonoid M] {l : List M} : l.sum = 0 ↔ ∀ x ∈ l, x = 0

theorem List.prod_eq_one_iff {M : Type u_3} [CanonicallyOrderedCommMonoid M] {l : List M} : l.prod = 1 ↔ ∀ x ∈ l, 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