mathlib documentation

data.list.big_operators

Sums and products from lists #

This file provides basic results about list.prod and list.sum, which calculate the product and sum of elements of a list. These are defined in data.list.defs.

source
@[simp]
theorem list.sum_nil {α : Type u_1} [add_monoid α] :
list.nil.sum = 0
source
@[simp]
theorem list.prod_nil {α : Type u_1} [monoid α] :
list.nil.prod = 1
source
theorem list.sum_singleton {α : Type u_1} [add_monoid α] {a : α} :
[a].sum = a
source
theorem list.prod_singleton {α : Type u_1} [monoid α] {a : α} :
[a].prod = a
source
@[simp]
theorem list.sum_cons {α : Type u_1} [add_monoid α] {l : list α} {a : α} :
(a :: l).sum = a + l.sum
source
@[simp]
theorem list.prod_cons {α : Type u_1} [monoid α] {l : list α} {a : α} :
(a :: l).prod = a * l.prod
source
@[simp]
theorem list.prod_append {α : Type u_1} [monoid α] {l₁ l₂ : list α} :
(l₁ ++ l₂).prod = (l₁.prod) * l₂.prod
source
@[simp]
theorem list.sum_append {α : Type u_1} [add_monoid α] {l₁ l₂ : list α} :
(l₁ ++ l₂).sum = l₁.sum + l₂.sum
source
theorem list.sum_concat {α : Type u_1} [add_monoid α] {l : list α} {a : α} :
(l.concat a).sum = l.sum + a
source
theorem list.prod_concat {α : Type u_1} [monoid α] {l : list α} {a : α} :
(l.concat a).prod = (l.prod) * a
source
@[simp]
theorem list.sum_join {α : Type u_1} [add_monoid α] {l : list (list α)} :
l.join.sum = (list.map list.sum l).sum
source
@[simp]
theorem list.prod_join {α : Type u_1} [monoid α] {l : list (list α)} :
l.join.prod = (list.map list.prod l).prod
source
theorem list.prod_eq_zero {M₀ : Type u_1} [monoid_with_zero M₀] {L : list M₀} (h : 0 ∈ L) :
L.prod = 0

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.

source
@[simp]
theorem list.prod_eq_zero_iff {M₀ : Type u_1} [monoid_with_zero M₀] [nontrivial M₀] [no_zero_divisors M₀] {L : list M₀} :
L.prod = 0 ↔ 0 ∈ L

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.

source
theorem list.prod_ne_zero {M₀ : Type u_1} [monoid_with_zero M₀] [nontrivial M₀] [no_zero_divisors M₀] {L : list M₀} (hL : 0 ∉ L) :
L.prod ≠ 0
source
theorem list.sum_eq_foldr {α : Type u_1} [add_monoid α] {l : list α} :
l.sum = list.foldr has_add.add 0 l
source
theorem list.prod_eq_foldr {α : Type u_1} [monoid α] {l : list α} :
l.prod = list.foldr has_mul.mul 1 l
source
theorem list.prod_hom_rel {α : Type u_1} {β : Type u_2} {γ : Type u_3} [monoid β] [monoid γ] (l : list α) {r : β → γ → Prop} {f : α → β} {g : α → γ} (h₁ : r 1 1) (h₂ : ∀ ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄, r b c → r ((f a) * b) ((g a) * c)) :
r (list.map f l).prod (list.map g l).prod
source
theorem list.sum_hom_rel {α : Type u_1} {β : Type u_2} {γ : Type u_3} [add_monoid β] [add_monoid γ] (l : list α) {r : β → γ → Prop} {f : α → β} {g : α → γ} (h₁ : r 0 0) (h₂ : ∀ ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄, r b c → r (f a + b) (g a + c)) :
r (list.map f l).sum (list.map g l).sum
source
theorem list.sum_hom {α : Type u_1} {β : Type u_2} [add_monoid α] [add_monoid β] (l : list α) (f : α →+ β) :
(list.map ⇑f l).sum = ⇑f l.sum
source
theorem list.prod_hom {α : Type u_1} {β : Type u_2} [monoid α] [monoid β] (l : list α) (f : α →* β) :
(list.map ⇑f l).prod = ⇑f l.prod
source
theorem list.sum_is_unit {β : Type u_2} [add_monoid β] {L : list β} (u : ∀ (m : β), m ∈ L → is_add_unit m) :
is_add_unit L.sum
source
theorem list.prod_is_unit {β : Type u_2} [monoid β] {L : list β} (u : ∀ (m : β), m ∈ L → is_unit m) :
is_unit L.prod
source
@[simp]
theorem list.sum_take_add_sum_drop {α : Type u_1} [add_monoid α] (L : list α) (i : ℕ) :
(list.take i L).sum + (list.drop i L).sum = L.sum
source
@[simp]
theorem list.prod_take_mul_prod_drop {α : Type u_1} [monoid α] (L : list α) (i : ℕ) :
((list.take i L).prod) * (list.drop i L).prod = L.prod
source
@[simp]
theorem list.sum_take_succ {α : Type u_1} [add_monoid α] (L : list α) (i : ℕ) (p : i < L.length) :
(list.take (i + 1) L).sum = (list.take i L).sum + L.nth_le i p
source
@[simp]
theorem list.prod_take_succ {α : Type u_1} [monoid α] (L : list α) (i : ℕ) (p : i < L.length) :
(list.take (i + 1) L).prod = ((list.take i L).prod) * L.nth_le i p
source
theorem list.length_pos_of_prod_ne_one {α : Type u_1} [monoid α] (L : list α) (h : L.prod ≠ 1) :
0 < L.length

A list with product not one must have positive length.

source
theorem list.length_pos_of_sum_ne_zero {α : Type u_1} [add_monoid α] (L : list α) (h : L.sum ≠ 0) :
0 < L.length
source
theorem list.prod_update_nth {α : Type u_1} [monoid α] (L : list α) (n : ℕ) (a : α) :
(L.update_nth n a).prod = (((list.take n L).prod) * ite (n < L.length) a 1) * (list.drop (n + 1) L).prod
source
theorem list.sum_update_nth {α : Type u_1} [add_monoid α] (L : list α) (n : ℕ) (a : α) :
(L.update_nth n a).sum = (list.take n L).sum + ite (n < L.length) a 0 + (list.drop (n + 1) L).sum
source
theorem mul_opposite.op_list_prod {α : Type u_1} [monoid α] (l : list α) :
mul_opposite.op l.prod = (list.map mul_opposite.op l).reverse.prod
source
theorem mul_opposite.unop_list_prod {α : Type u_1} [monoid α] (l : list αᵐᵒᵖ) :
mul_opposite.unop l.prod = (list.map mul_opposite.unop l).reverse.prod
source
theorem list.prod_inv_reverse {α : Type u_1} [group α] (L : list α) :
(L.prod)⁻¹ = (list.map (λ (x : α), x⁻¹) L).reverse.prod

This is the list.prod version of mul_inv_rev

source
theorem list.sum_neg_reverse {α : Type u_1} [add_group α] (L : list α) :
-L.sum = (list.map (λ (x : α), -x) L).reverse.sum

This is the list.sum version of add_neg_rev

source
theorem list.prod_reverse_noncomm {α : Type u_1} [group α] (L : list α) :
L.reverse.prod = ((list.map (λ (x : α), x⁻¹) L).prod)⁻¹

A non-commutative variant of list.prod_reverse

source
theorem list.sum_reverse_noncomm {α : Type u_1} [add_group α] (L : list α) :
L.reverse.sum = -(list.map (λ (x : α), -x) L).sum

A non-commutative variant of list.sum_reverse

source
@[simp]
theorem list.sum_drop_succ {α : Type u_1} [add_group α] (L : list α) (i : ℕ) (p : i < L.length) :
(list.drop (i + 1) L).sum = -L.nth_le i p + (list.drop i L).sum

Counterpart to list.sum_take_succ when we have an negation operation

source
@[simp]
theorem list.prod_drop_succ {α : Type u_1} [group α] (L : list α) (i : ℕ) (p : i < L.length) :
(list.drop (i + 1) L).prod = (L.nth_le i p)⁻¹ * (list.drop i L).prod

Counterpart to list.prod_take_succ when we have an inverse operation

source
theorem list.sum_neg {α : Type u_1} [add_comm_group α] (L : list α) :
-L.sum = (list.map (λ (x : α), -x) L).sum

This is the list.sum version of add_neg

source
theorem list.prod_inv {α : Type u_1} [comm_group α] (L : list α) :
(L.prod)⁻¹ = (list.map (λ (x : α), x⁻¹) L).prod

This is the list.prod version of mul_inv

source
theorem list.prod_update_nth' {α : Type u_1} [comm_group α] (L : list α) (n : ℕ) (a : α) :
(L.update_nth n a).prod = (L.prod) * dite (n < L.length) (λ (hn : n < L.length), (L.nth_le n hn)⁻¹ * a) (λ (hn : ¬n < L.length), 1)

Alternative version of list.prod_update_nth when the list is over a group

source
theorem list.sum_update_nth' {α : Type u_1} [add_comm_group α] (L : list α) (n : ℕ) (a : α) :
(L.update_nth n a).sum = L.sum + dite (n < L.length) (λ (hn : n < L.length), -L.nth_le n hn + a) (λ (hn : ¬n < L.length), 0)

Alternative version of list.sum_update_nth when the list is over a group

source
theorem list.eq_of_sum_take_eq {α : Type u_1} [add_left_cancel_monoid α] {L L' : list α} (h : L.length = L'.length) (h' : ∀ (i : ℕ), i ≤ L.length → (list.take i L).sum = (list.take i L').sum) :
L = L'
source
theorem list.monotone_sum_take {α : Type u_1} [canonically_ordered_add_monoid α] (L : list α) :
monotone (λ (i : ℕ), (list.take i L).sum)
source
theorem list.sum_nonneg {α : Type u_1} [ordered_add_comm_monoid α] {l : list α} (hl₁ : ∀ (x : α), x ∈ l → 0 ≤ x) :
0 ≤ l.sum
source
theorem list.one_le_prod_of_one_le {α : Type u_1} [ordered_comm_monoid α] {l : list α} (hl₁ : ∀ (x : α), x ∈ l → 1 ≤ x) :
1 ≤ l.prod
source
theorem list.one_lt_prod_of_one_lt {α : Type u_1} [ordered_comm_monoid α] (l : list α) (hl : ∀ (x : α), x ∈ l → 1 < x) (hl₂ : l ≠ list.nil) :
1 < l.prod
source
theorem list.sum_pos {α : Type u_1} [ordered_add_comm_monoid α] (l : list α) (hl : ∀ (x : α), x ∈ l → 0 < x) (hl₂ : l ≠ list.nil) :
0 < l.sum
source
theorem list.single_le_sum {α : Type u_1} [ordered_add_comm_monoid α] {l : list α} (hl₁ : ∀ (x : α), x ∈ l → 0 ≤ x) (x : α) (H : x ∈ l) :
x ≤ l.sum
source
theorem list.single_le_prod {α : Type u_1} [ordered_comm_monoid α] {l : list α} (hl₁ : ∀ (x : α), x ∈ l → 1 ≤ x) (x : α) (H : x ∈ l) :
x ≤ l.prod
source
theorem list.all_zero_of_le_zero_le_of_sum_eq_zero {α : Type u_1} [ordered_add_comm_monoid α] {l : list α} (hl₁ : ∀ (x : α), x ∈ l → 0 ≤ x) (hl₂ : l.sum = 0) {x : α} (hx : x ∈ l) :
x = 0
source
theorem list.all_one_of_le_one_le_of_prod_eq_one {α : Type u_1} [ordered_comm_monoid α] {l : list α} (hl₁ : ∀ (x : α), x ∈ l → 1 ≤ x) (hl₂ : l.prod = 1) {x : α} (hx : x ∈ l) :
x = 1
source
theorem list.sum_eq_zero_iff {α : Type u_1} [canonically_ordered_add_monoid α] (l : list α) :
l.sum = 0 ↔ ∀ (x : α), x ∈ l → x = 0
source
theorem list.length_le_sum_of_one_le (L : list ℕ) (h : ∀ (i : ℕ), i ∈ L → 1 ≤ i) :
L.length ≤ L.sum

If all elements in a list are bounded below by 1, then the length of the list is bounded by the sum of the elements.

source
theorem list.length_pos_of_sum_pos {α : Type u_1} [ordered_cancel_add_comm_monoid α] (L : list α) (h : 0 < L.sum) :
0 < L.length

A list with positive sum must have positive length.

source
theorem list.sum_le_foldr_max {α : Type u_1} {β : Type u_2} [add_monoid α] [add_monoid β] [linear_order β] (f : α → β) (h0 : f 0 ≤ 0) (hadd : ∀ (x y : α), f (x + y) ≤ max (f x) (f y)) (l : list α) :
f l.sum ≤ list.foldr max 0 (list.map f l)
source
@[simp]
theorem list.sum_erase {α : Type u_1} [decidable_eq α] [add_comm_monoid α] {a : α} {l : list α} :
a ∈ l → a + (l.erase a).sum = l.sum
source
@[simp]
theorem list.prod_erase {α : Type u_1} [decidable_eq α] [comm_monoid α] {a : α} {l : list α} :
a ∈ l → a * (l.erase a).prod = l.prod
source
theorem list.dvd_prod {α : Type u_1} [comm_monoid α] {a : α} {l : list α} (ha : a ∈ l) :
a ∣ l.prod
source
@[simp]
theorem list.sum_const_nat (m n : ℕ) :
(list.repeat m n).sum = m * n
source
theorem list.dvd_sum {α : Type u_1} [comm_semiring α] {a : α} {l : list α} (h : ∀ (x : α), x ∈ l → a ∣ x) :
a ∣ l.sum
source
theorem list.exists_lt_of_sum_lt {α : Type u_1} {β : Type u_2} [linear_ordered_cancel_add_comm_monoid β] {l : list α} (f g : α → β) (h : (list.map f l).sum < (list.map g l).sum) :
∃ (x : α) (H : x ∈ l), f x < g x
source
theorem list.exists_le_of_sum_le {α : Type u_1} {β : Type u_2} [linear_ordered_cancel_add_comm_monoid β] {l : list α} (hl : l ≠ list.nil) (f g : α → β) (h : (list.map f l).sum ≤ (list.map g l).sum) :
∃ (x : α) (H : x ∈ l), f x ≤ g x
source
theorem list.nth_zero_add_tail_sum {α : Type u_1} [add_monoid α] (l : list α) :
(l.nth 0).get_or_else 0 + l.tail.sum = l.sum
source
theorem list.nth_zero_mul_tail_prod {α : Type u_1} [monoid α] (l : list α) :
((l.nth 0).get_or_else 1) * l.tail.prod = l.prod

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 and state the lemma for ℕ as

source
theorem list.head_add_tail_sum_of_ne_nil {α : Type u_1} [add_monoid α] [inhabited α] (l : list α) (h : l ≠ list.nil) :
l.head + l.tail.sum = l.sum
source
theorem list.head_mul_tail_prod_of_ne_nil {α : Type u_1} [monoid α] [inhabited α] (l : list α) (h : l ≠ list.nil) :
(l.head) * l.tail.prod = l.prod

Same as nth_zero_mul_tail_prod, but avoiding the list.head garbage complication by requiring the list to be nonempty.

source
theorem list.prod_pos {α : Type u_1} [ordered_semiring α] [nontrivial α] (l : list α) (h : ∀ (a : α), a ∈ l → 0 < a) :
0 < l.prod

The product of a list of positive natural numbers is positive, and likewise for any nontrivial ordered 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.

source
theorem list.head_add_tail_sum (L : list ℕ) :
L.head + L.tail.sum = L.sum

This relies on default ℕ = 0.

source
theorem list.head_le_sum (L : list ℕ) :
L.head ≤ L.sum

This relies on default ℕ = 0.

source
theorem list.tail_sum (L : list ℕ) :
L.tail.sum = L.sum - L.head

This relies on default ℕ = 0.

source
@[simp]
theorem list.alternating_sum_nil {G : Type u_4} [add_comm_group G] :
list.nil.alternating_sum = 0
source
@[simp]
theorem list.alternating_prod_nil {G : Type u_4} [comm_group G] :
list.nil.alternating_prod = 1
source
@[simp]
theorem list.alternating_prod_singleton {G : Type u_4} [comm_group G] (g : G) :
[g].alternating_prod = g
source
@[simp]
theorem list.alternating_sum_singleton {G : Type u_4} [add_comm_group G] (g : G) :
[g].alternating_sum = g
source
@[simp]
theorem list.alternating_sum_cons_cons' {G : Type u_4} [add_comm_group G] (g h : G) (l : list G) :
(g :: h :: l).alternating_sum = g + -h + l.alternating_sum
source
@[simp]
theorem list.alternating_prod_cons_cons {G : Type u_4} [comm_group G] (g h : G) (l : list G) :
(g :: h :: l).alternating_prod = (g * h⁻¹) * l.alternating_prod
source
theorem list.alternating_sum_cons_cons {G : Type u_1} [add_comm_group G] (g h : G) (l : list G) :
(g :: h :: l).alternating_sum = g - h + l.alternating_sum
source
theorem monoid_hom.map_list_prod {α : Type u_1} {β : Type u_2} [monoid α] [monoid β] (f : α →* β) (l : list α) :
⇑f l.prod = (list.map ⇑f l).prod
source
theorem add_monoid_hom.map_list_sum {α : Type u_1} {β : Type u_2} [add_monoid α] [add_monoid β] (f : α →+ β) (l : list α) :
⇑f l.sum = (list.map ⇑f l).sum
source
theorem monoid_hom.unop_map_list_prod {α : Type u_1} {β : Type u_2} [monoid α] [monoid β] (f : α →* βᵐᵒᵖ) (l : list α) :
mul_opposite.unop (⇑f l.prod) = (list.map (mul_opposite.unop ∘ ⇑f) l).reverse.prod

A morphism into the opposite monoid acts on the product by acting on the reversed elements

source
theorem list.prod_map_hom {α : Type u_1} {β : Type u_2} {γ : Type u_3} [monoid β] [monoid γ] (L : list α) (f : α → β) (g : β →* γ) :
(list.map (⇑g ∘ f) L).prod = ⇑g (list.map f L).prod
source
theorem list.sum_map_hom {α : Type u_1} {β : Type u_2} {γ : Type u_3} [add_monoid β] [add_monoid γ] (L : list α) (f : α → β) (g : β →+ γ) :
(list.map (⇑g ∘ f) L).sum = ⇑g (list.map f L).sum
source
theorem list.sum_map_mul_left {α : Type u_1} {β : Type u_2} [semiring α] (L : list β) (f : β → α) (r : α) :
(list.map (λ (b : β), r * f b) L).sum = r * (list.map f L).sum
source
theorem list.sum_map_mul_right {α : Type u_1} {β : Type u_2} [semiring α] (L : list β) (f : β → α) (r : α) :
(list.map (λ (b : β), (f b) * r) L).sum = ((list.map f L).sum) * r