Sums and products from lists #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This file provides basic results about list.prod, list.sum, which calculate the product and sum
of elements of a list and list.alternating_prod, list.alternating_sum, their alternating
counterparts. These are defined in data.list.defs.
@[simp]
theorem
list.sum_eq_foldr
{M : Type u_3}
[add_monoid M]
{l : list M} :
l.sum = list.foldr has_add.add 0 l
theorem
list.prod_eq_foldr
{M : Type u_3}
[monoid M]
{l : list M} :
l.prod = list.foldr has_mul.mul 1 l
@[simp]
theorem
list.prod_replicate
{M : Type u_3}
[monoid M]
(n : ℕ)
(a : M) :
(list.replicate n a).prod = a ^ n
@[simp]
theorem
list.sum_replicate
{M : Type u_3}
[add_monoid M]
(n : ℕ)
(a : M) :
(list.replicate n a).sum = n • a
theorem
list.sum_hom
{M : Type u_3}
{N : Type u_4}
[add_monoid M]
[add_monoid N]
(l : list M)
{F : Type u_1}
[add_monoid_hom_class F M N]
(f : F) :
theorem
list.sum_hom₂
{ι : Type u_1}
{M : Type u_3}
{N : Type u_4}
{P : Type u_5}
[add_monoid M]
[add_monoid N]
[add_monoid P]
(l : list ι)
(f : M → N → P)
(hf : ∀ (a b : M) (c d : N), f (a + b) (c + d) = f a c + f b d)
(hf' : f 0 0 = 0)
(f₁ : ι → M)
(f₂ : ι → N) :
@[simp]
theorem
list.sum_map_hom
{ι : Type u_1}
{M : Type u_3}
{N : Type u_4}
[add_monoid M]
[add_monoid N]
(L : list ι)
(f : ι → M)
{G : Type u_2}
[add_monoid_hom_class G M N]
(g : G) :
theorem
list.sum_is_add_unit
{M : Type u_3}
[add_monoid M]
{L : list M}
(u : ∀ (m : M), m ∈ L → is_add_unit m) :
theorem
list.sum_is_add_unit_iff
{α : Type u_1}
[add_comm_monoid α]
{L : list α} :
is_add_unit L.sum ↔ ∀ (m : α), m ∈ L → is_add_unit m
A list with sum not zero must have positive length.
theorem
list.length_pos_of_sum_pos
{M : Type u_3}
[add_monoid M]
[preorder M]
(L : list M)
(h : 0 < L.sum) :
A list with positive sum must have positive length.
theorem
list.length_pos_of_sum_neg
{M : Type u_3}
[add_monoid M]
[preorder M]
(L : list M)
(h : L.sum < 0) :
A list with negative sum must have positive length.
We'd like to state this as L.head + L.tail.sum = L.sum, but because L.head
relies on an inhabited instance to return a garbage value on the empty list, this is not possible.
Instead, we write the statement in terms of (L.nth 0).get_or_else 0.
We'd like to state this as L.head * L.tail.prod = L.prod, but because L.head relies on an
inhabited instance to return a garbage value on the empty list, this is not possible.
Instead, we write the statement in terms of (L.nth 0).get_or_else 1.
theorem
add_commute.list_sum_right
{M : Type u_3}
[add_monoid M]
(l : list M)
(y : M)
(h : ∀ (x : M), x ∈ l → add_commute y x) :
add_commute y l.sum
theorem
add_commute.list_sum_left
{M : Type u_3}
[add_monoid M]
(l : list M)
(y : M)
(h : ∀ (x : M), x ∈ l → add_commute x y) :
add_commute l.sum y
theorem
list.forall₂.sum_le_sum
{M : Type u_3}
[add_monoid M]
[preorder M]
[covariant_class M M (function.swap has_add.add) has_le.le]
[covariant_class M M has_add.add has_le.le]
{l₁ l₂ : list M}
(h : list.forall₂ has_le.le l₁ l₂) :
theorem
list.forall₂.prod_le_prod'
{M : Type u_3}
[monoid M]
[preorder M]
[covariant_class M M (function.swap has_mul.mul) has_le.le]
[covariant_class M M has_mul.mul has_le.le]
{l₁ l₂ : list M}
(h : list.forall₂ has_le.le l₁ l₂) :
theorem
list.sublist.sum_le_sum
{M : Type u_3}
[add_monoid M]
[preorder M]
[covariant_class M M (function.swap has_add.add) has_le.le]
[covariant_class M M has_add.add has_le.le]
{l₁ l₂ : list M}
(h : l₁ <+ l₂)
(h₁ : ∀ (a : M), a ∈ l₂ → 0 ≤ a) :
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]
[covariant_class M M (function.swap has_mul.mul) has_le.le]
[covariant_class M M has_mul.mul has_le.le]
{l₁ l₂ : list M}
(h : l₁ <+ l₂)
(h₁ : ∀ (a : M), a ∈ l₂ → 1 ≤ a) :
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.sublist_forall₂.sum_le_sum
{M : Type u_3}
[add_monoid M]
[preorder M]
[covariant_class M M (function.swap has_add.add) has_le.le]
[covariant_class M M has_add.add has_le.le]
{l₁ l₂ : list M}
(h : list.sublist_forall₂ has_le.le l₁ l₂)
(h₁ : ∀ (a : M), a ∈ l₂ → 0 ≤ a) :
theorem
list.sublist_forall₂.prod_le_prod'
{M : Type u_3}
[monoid M]
[preorder M]
[covariant_class M M (function.swap has_mul.mul) has_le.le]
[covariant_class M M has_mul.mul has_le.le]
{l₁ l₂ : list M}
(h : list.sublist_forall₂ has_le.le l₁ l₂)
(h₁ : ∀ (a : M), a ∈ l₂ → 1 ≤ a) :
theorem
list.sum_le_sum
{ι : Type u_1}
{M : Type u_3}
[add_monoid M]
[preorder M]
[covariant_class M M (function.swap has_add.add) has_le.le]
[covariant_class M M has_add.add has_le.le]
{l : list ι}
{f g : ι → M}
(h : ∀ (i : ι), i ∈ l → f i ≤ g i) :
theorem
list.prod_le_prod'
{ι : Type u_1}
{M : Type u_3}
[monoid M]
[preorder M]
[covariant_class M M (function.swap has_mul.mul) has_le.le]
[covariant_class M M has_mul.mul has_le.le]
{l : list ι}
{f g : ι → M}
(h : ∀ (i : ι), i ∈ l → f i ≤ g i) :
theorem
list.prod_lt_prod'
{ι : Type u_1}
{M : Type u_3}
[monoid M]
[preorder M]
[covariant_class M M has_mul.mul has_lt.lt]
[covariant_class M M has_mul.mul has_le.le]
[covariant_class M M (function.swap has_mul.mul) has_lt.lt]
[covariant_class M M (function.swap has_mul.mul) has_le.le]
{l : list ι}
(f g : ι → M)
(h₁ : ∀ (i : ι), i ∈ l → f i ≤ g i)
(h₂ : ∃ (i : ι) (H : i ∈ l), f i < g i) :
theorem
list.sum_lt_sum
{ι : Type u_1}
{M : Type u_3}
[add_monoid M]
[preorder M]
[covariant_class M M has_add.add has_lt.lt]
[covariant_class M M has_add.add has_le.le]
[covariant_class M M (function.swap has_add.add) has_lt.lt]
[covariant_class M M (function.swap has_add.add) has_le.le]
{l : list ι}
(f g : ι → M)
(h₁ : ∀ (i : ι), i ∈ l → f i ≤ g i)
(h₂ : ∃ (i : ι) (H : i ∈ l), f i < g i) :
theorem
list.sum_lt_sum_of_ne_nil
{ι : Type u_1}
{M : Type u_3}
[add_monoid M]
[preorder M]
[covariant_class M M has_add.add has_lt.lt]
[covariant_class M M has_add.add has_le.le]
[covariant_class M M (function.swap has_add.add) has_lt.lt]
[covariant_class M M (function.swap has_add.add) has_le.le]
{l : list ι}
(hl : l ≠ list.nil)
(f g : ι → M)
(hlt : ∀ (i : ι), 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]
[covariant_class M M has_mul.mul has_lt.lt]
[covariant_class M M has_mul.mul has_le.le]
[covariant_class M M (function.swap has_mul.mul) has_lt.lt]
[covariant_class M M (function.swap has_mul.mul) has_le.le]
{l : list ι}
(hl : l ≠ list.nil)
(f g : ι → M)
(hlt : ∀ (i : ι), i ∈ l → f i < g i) :
theorem
list.prod_le_pow_card
{M : Type u_3}
[monoid M]
[preorder M]
[covariant_class M M (function.swap has_mul.mul) has_le.le]
[covariant_class M M has_mul.mul has_le.le]
(l : list M)
(n : M)
(h : ∀ (x : M), x ∈ l → x ≤ n) :
theorem
list.sum_le_card_nsmul
{M : Type u_3}
[add_monoid M]
[preorder M]
[covariant_class M M (function.swap has_add.add) has_le.le]
[covariant_class M M has_add.add has_le.le]
(l : list M)
(n : M)
(h : ∀ (x : M), x ∈ l → x ≤ n) :
theorem
list.exists_lt_of_prod_lt'
{ι : Type u_1}
{M : Type u_3}
[monoid M]
[linear_order M]
[covariant_class M M (function.swap has_mul.mul) has_le.le]
[covariant_class M M has_mul.mul has_le.le]
{l : list ι}
(f g : ι → M)
(h : (list.map f l).prod < (list.map g l).prod) :
theorem
list.exists_lt_of_sum_lt
{ι : Type u_1}
{M : Type u_3}
[add_monoid M]
[linear_order M]
[covariant_class M M (function.swap has_add.add) has_le.le]
[covariant_class M M has_add.add has_le.le]
{l : list ι}
(f g : ι → M)
(h : (list.map f l).sum < (list.map g l).sum) :
theorem
list.exists_le_of_sum_le
{ι : Type u_1}
{M : Type u_3}
[add_monoid M]
[linear_order M]
[covariant_class M M has_add.add has_lt.lt]
[covariant_class M M has_add.add has_le.le]
[covariant_class M M (function.swap has_add.add) has_lt.lt]
[covariant_class M M (function.swap has_add.add) has_le.le]
{l : list ι}
(hl : l ≠ list.nil)
(f g : ι → M)
(h : (list.map f l).sum ≤ (list.map g l).sum) :
theorem
list.exists_le_of_prod_le'
{ι : Type u_1}
{M : Type u_3}
[monoid M]
[linear_order M]
[covariant_class M M has_mul.mul has_lt.lt]
[covariant_class M M has_mul.mul has_le.le]
[covariant_class M M (function.swap has_mul.mul) has_lt.lt]
[covariant_class M M (function.swap has_mul.mul) has_le.le]
{l : list ι}
(hl : l ≠ list.nil)
(f g : ι → M)
(h : (list.map f l).prod ≤ (list.map g l).prod) :
theorem
list.sum_nonneg
{M : Type u_3}
[add_monoid M]
[preorder M]
[covariant_class M M has_add.add has_le.le]
{l : list M}
(hl₁ : ∀ (x : M), x ∈ l → 0 ≤ x) :
theorem
list.one_le_prod_of_one_le
{M : Type u_3}
[monoid M]
[preorder M]
[covariant_class M M has_mul.mul has_le.le]
{l : list M}
(hl₁ : ∀ (x : M), x ∈ l → 1 ≤ x) :
If zero is an element of a list L, then list.prod L = 0. If the domain is a nontrivial
monoid with zero with no divisors, then this implication becomes an iff, see
list.prod_eq_zero_iff.
@[simp]
theorem
list.prod_eq_zero_iff
{M₀ : Type u_6}
[monoid_with_zero M₀]
[nontrivial M₀]
[no_zero_divisors M₀]
{L : list M₀} :
Product of elements of a list L equals zero if and only if 0 ∈ L. See also
list.prod_eq_zero for an implication that needs weaker typeclass assumptions.
theorem
list.prod_ne_zero
{M₀ : Type u_6}
[monoid_with_zero M₀]
[nontrivial M₀]
[no_zero_divisors M₀]
{L : list M₀}
(hL : 0 ∉ L) :
Alternative version of list.prod_update_nth when the list is over a group
theorem
list.sum_eq_zero
{M : Type u_3}
[add_monoid M]
{l : list M}
(hl : ∀ (x : M), x ∈ l → x = 0) :
Slightly more general version of list.sum_eq_zero_iff
for a non-ordered add_monoid
theorem
list.sum_le_foldr_max
{M : Type u_3}
{N : Type u_4}
[add_monoid M]
[add_monoid N]
[linear_order N]
(f : M → N)
(h0 : f 0 ≤ 0)
(hadd : ∀ (x y : M), f (x + y) ≤ linear_order.max (f x) (f y))
(l : list M) :
f l.sum ≤ list.foldr linear_order.max 0 (list.map f l)
@[simp]
@[simp]
@[simp]
theorem
canonically_ordered_comm_semiring.list_prod_pos
{α : Type u_1}
[canonically_ordered_comm_semiring α]
[nontrivial α]
{l : list α} :
A variant of list.prod_pos for canonically_ordered_comm_semiring.
Several lemmas about sum/head/tail for list ℕ.
These are hard to generalize well, as they rely on the fact that default ℕ = 0.
If desired, we could add a class stating that default = 0.
@[simp]
@[simp]
@[simp]
theorem
list.alternating_prod_singleton
{α : Type u_2}
[has_one α]
[has_mul α]
[has_inv α]
(a : α) :
[a].alternating_prod = a
@[simp]
theorem
list.alternating_sum_singleton
{α : Type u_2}
[has_zero α]
[has_add α]
[has_neg α]
(a : α) :
[a].alternating_sum = a
theorem
list.alternating_prod_cons_cons'
{α : Type u_2}
[has_one α]
[has_mul α]
[has_inv α]
(a b : α)
(l : list α) :
(a :: b :: l).alternating_prod = a * b⁻¹ * l.alternating_prod
theorem
list.alternating_sum_cons_cons'
{α : Type u_2}
[has_zero α]
[has_add α]
[has_neg α]
(a b : α)
(l : list α) :
(a :: b :: l).alternating_sum = a + -b + l.alternating_sum
theorem
list.alternating_prod_cons_cons
{α : Type u_2}
[div_inv_monoid α]
(a b : α)
(l : list α) :
(a :: b :: l).alternating_prod = a / b * l.alternating_prod
theorem
list.alternating_sum_cons_cons
{α : Type u_2}
[sub_neg_monoid α]
(a b : α)
(l : list α) :
(a :: b :: l).alternating_sum = a - b + l.alternating_sum
theorem
list.alternating_prod_cons'
{α : Type u_2}
[comm_group α]
(a : α)
(l : list α) :
(a :: l).alternating_prod = a * (l.alternating_prod)⁻¹
theorem
list.alternating_sum_cons'
{α : Type u_2}
[add_comm_group α]
(a : α)
(l : list α) :
(a :: l).alternating_sum = a + -l.alternating_sum
@[simp]
theorem
list.alternating_prod_cons
{α : Type u_2}
[comm_group α]
(a : α)
(l : list α) :
(a :: l).alternating_prod = a / l.alternating_prod
@[simp]
theorem
list.alternating_sum_cons
{α : Type u_2}
[add_comm_group α]
(a : α)
(l : list α) :
(a :: l).alternating_sum = a - l.alternating_sum
theorem
map_list_sum
{M : Type u_3}
{N : Type u_4}
[add_monoid M]
[add_monoid N]
{F : Type u_1}
[add_monoid_hom_class F M N]
(f : F)
(l : list M) :
@[protected]
theorem
add_monoid_hom.map_list_sum
{M : Type u_3}
{N : Type u_4}
[add_monoid M]
[add_monoid N]
(f : M →+ N)
(l : list M) :
Deprecated, use _root_.map_list_sum instead.