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 (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₁ : 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 (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₁ : 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.

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₁ : 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 (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₁ : 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 (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 : 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 (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 : 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 (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₁ : 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 (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₁ : 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 (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 : 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 (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 : 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 (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 : 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 (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 : 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 (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 : 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 (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 : 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 (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) :
    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 (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) :
    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 (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) :
    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 (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) :
    xl, 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₁ : 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 (x x_1 : M) => x * x_1) fun (x x_1 : M) => x x_1] {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)
    abbrev List.sum_pos.match_1 {M : Type u_1} [OrderedAddCommMonoid M] (motive : (x : List M) → (x_1x, 0 < x_1)x []Prop) :
    ∀ (x : List M) (x_1 : x_1x, 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₁ : xa :: 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.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
      theorem List.single_le_prod {M : Type u_3} [OrderedCommMonoid M] {l : List M} (hl₁ : xl, 1 x) (x : M) :
      x lx l.prod
      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