Sums and products from lists

This file provides basic results about List.prod, List.sum, which calculate the product and sum of elements of a list and List.alternatingProd, List.alternatingSum, their alternating counterparts. These are defined in Algebra.BigOperators.List.Defs.

@[simp]

theorem List.sum_nil {M : Type u_3} [AddZeroClass M] : List.sum [] = 0

@[simp]

theorem List.prod_nil {M : Type u_3} [MulOneClass M] : List.prod [] = 1

theorem List.sum_singleton {M : Type u_3} [AddZeroClass M] {a : M} : List.sum [a] = a

theorem List.prod_singleton {M : Type u_3} [MulOneClass M] {a : M} : List.prod [a] = a

@[simp]

theorem List.sum_zero_cons {M : Type u_3} [AddZeroClass M] {l : List M} : List.sum (0 :: l) = List.sum l

@[simp]

theorem List.prod_one_cons {M : Type u_3} [MulOneClass M] {l : List M} : List.prod (1 :: l) = List.prod l

theorem List.sum_map_zero {ι : Type u_1} {M : Type u_3} [AddZeroClass M] {l : List ι} : List.sum (List.map (fun (x : ι) => 0) l) = 0

theorem List.prod_map_one {ι : Type u_1} {M : Type u_3} [MulOneClass M] {l : List ι} : List.prod (List.map (fun (x : ι) => 1) l) = 1

@[simp]

theorem List.sum_cons {M : Type u_3} [AddMonoid M] {l : List M} {a : M} : List.sum (a :: l) = a + List.sum l

@[simp]

theorem List.prod_cons {M : Type u_3} [Monoid M] {l : List M} {a : M} : List.prod (a :: l) = a * List.prod l

theorem List.sum_induction {M : Type u_3} [AddMonoid M] {l : List M} (p : M → Prop) (hom : ∀ (a b : M), p a → p b → p (a + b)) (unit : p 0) (base : ∀ (x : M), x ∈ l → p x) : p (List.sum l)

theorem List.prod_induction {M : Type u_3} [Monoid M] {l : List M} (p : M → Prop) (hom : ∀ (a b : M), p a → p b → p (a * b)) (unit : p 1) (base : ∀ (x : M), x ∈ l → p x) : p (List.prod l)

@[simp]

theorem List.sum_append {M : Type u_3} [AddMonoid M] {l₁ : List M} {l₂ : List M} : List.sum (l₁ ++ l₂) = List.sum l₁ + List.sum l₂

@[simp]

theorem List.prod_append {M : Type u_3} [Monoid M] {l₁ : List M} {l₂ : List M} : List.prod (l₁ ++ l₂) = List.prod l₁ * List.prod l₂

theorem List.sum_concat {M : Type u_3} [AddMonoid M] {l : List M} {a : M} : List.sum (List.concat l a) = List.sum l + a

theorem List.prod_concat {M : Type u_3} [Monoid M] {l : List M} {a : M} : List.prod (List.concat l a) = List.prod l * a

@[simp]

theorem List.sum_join {M : Type u_3} [AddMonoid M] {l : List (List M)} : List.sum (List.join l) = List.sum (List.map List.sum l)

@[simp]

theorem List.prod_join {M : Type u_3} [Monoid M] {l : List (List M)} : List.prod (List.join l) = List.prod (List.map List.prod l)

theorem List.sum_eq_foldr {M : Type u_3} [AddMonoid M] {l : List M} : List.sum l = List.foldr (fun (x x_1 : M) => x + x_1) 0 l

abbrev List.sum_eq_foldr.match_1 {M : Type u_1} (motive : List M → Prop) : ∀ (x : List M), (Unit → motive []) → (∀ (a : M) (l : List M), motive (a :: l)) → motive x

Equations

• ⋯ = ⋯

theorem List.prod_eq_foldr {M : Type u_3} [Monoid M] {l : List M} : List.prod l = List.foldr (fun (x x_1 : M) => x * x_1) 1 l

@[simp]

theorem List.sum_replicate {M : Type u_3} [AddMonoid M] (n : ℕ) (a : M) : List.sum (List.replicate n a) = n • a

@[simp]

theorem List.prod_replicate {M : Type u_3} [Monoid M] (n : ℕ) (a : M) : List.prod (List.replicate n a) = a ^ n

theorem List.sum_eq_card_nsmul {M : Type u_3} [AddMonoid M] (l : List M) (m : M) (h : ∀ (x : M), x ∈ l → x = m) : List.sum l = List.length l • m

theorem List.prod_eq_pow_card {M : Type u_3} [Monoid M] (l : List M) (m : M) (h : ∀ (x : M), x ∈ l → x = m) : List.prod l = m ^ List.length l

theorem List.sum_hom_rel {ι : Type u_1} {M : Type u_3} {N : Type u_4} [AddMonoid M] [AddMonoid N] (l : List ι) {r : M → N → Prop} {f : ι → M} {g : ι → N} (h₁ : r 0 0) (h₂ : ∀ ⦃i : ι⦄ ⦃a : M⦄ ⦃b : N⦄, r a b → r (f i + a) (g i + b)) : r (List.sum (List.map f l)) (List.sum (List.map g l))

theorem List.prod_hom_rel {ι : Type u_1} {M : Type u_3} {N : Type u_4} [Monoid M] [Monoid N] (l : List ι) {r : M → N → Prop} {f : ι → M} {g : ι → N} (h₁ : r 1 1) (h₂ : ∀ ⦃i : ι⦄ ⦃a : M⦄ ⦃b : N⦄, r a b → r (f i * a) (g i * b)) : r (List.prod (List.map f l)) (List.prod (List.map g l))

theorem List.rel_sum {M : Type u_3} {N : Type u_4} [AddMonoid M] [AddMonoid N] {R : M → N → Prop} (h : R 0 0) (hf : (R ⇒ R ⇒ R) (fun (x x_1 : M) => x + x_1) fun (x x_1 : N) => x + x_1) : (List.Forall₂ R ⇒ R) List.sum List.sum

theorem List.rel_prod {M : Type u_3} {N : Type u_4} [Monoid M] [Monoid N] {R : M → N → Prop} (h : R 1 1) (hf : (R ⇒ R ⇒ R) (fun (x x_1 : M) => x * x_1) fun (x x_1 : N) => x * x_1) : (List.Forall₂ R ⇒ R) List.prod List.prod

theorem List.sum_hom {M : Type u_3} {N : Type u_4} [AddMonoid M] [AddMonoid N] (l : List M) {F : Type u_9} [FunLike F M N] [AddMonoidHomClass F M N] (f : F) : List.sum (List.map (⇑f) l) = f (List.sum l)

theorem List.prod_hom {M : Type u_3} {N : Type u_4} [Monoid M] [Monoid N] (l : List M) {F : Type u_9} [FunLike F M N] [MonoidHomClass F M N] (f : F) : List.prod (List.map (⇑f) l) = f (List.prod l)

theorem List.sum_hom₂ {ι : Type u_1} {M : Type u_3} {N : Type u_4} {P : Type u_5} [AddMonoid M] [AddMonoid N] [AddMonoid 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) : List.sum (List.map (fun (i : ι) => f (f₁ i) (f₂ i)) l) = f (List.sum (List.map f₁ l)) (List.sum (List.map f₂ l))

theorem List.prod_hom₂ {ι : Type u_1} {M : Type u_3} {N : Type u_4} {P : Type u_5} [Monoid M] [Monoid N] [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 1 1 = 1) (f₁ : ι → M) (f₂ : ι → N) : List.prod (List.map (fun (i : ι) => f (f₁ i) (f₂ i)) l) = f (List.prod (List.map f₁ l)) (List.prod (List.map f₂ l))

@[simp]

theorem List.sum_map_add {ι : Type u_1} {α : Type u_9} [AddCommMonoid α] {l : List ι} {f : ι → α} {g : ι → α} : List.sum (List.map (fun (i : ι) => f i + g i) l) = List.sum (List.map f l) + List.sum (List.map g l)

@[simp]

theorem List.prod_map_mul {ι : Type u_1} {α : Type u_9} [CommMonoid α] {l : List ι} {f : ι → α} {g : ι → α} : List.prod (List.map (fun (i : ι) => f i * g i) l) = List.prod (List.map f l) * List.prod (List.map g l)

@[simp]

theorem List.prod_map_neg {M : Type u_3} [Monoid M] [HasDistribNeg M] (l : List M) : List.prod (List.map Neg.neg l) = (-1) ^ List.length l * List.prod l

theorem List.sum_map_hom {ι : Type u_1} {M : Type u_3} {N : Type u_4} [AddMonoid M] [AddMonoid N] (L : List ι) (f : ι → M) {G : Type u_9} [FunLike G M N] [AddMonoidHomClass G M N] (g : G) : List.sum (List.map (⇑g ∘ f) L) = g (List.sum (List.map f L))

theorem List.prod_map_hom {ι : Type u_1} {M : Type u_3} {N : Type u_4} [Monoid M] [Monoid N] (L : List ι) (f : ι → M) {G : Type u_9} [FunLike G M N] [MonoidHomClass G M N] (g : G) : List.prod (List.map (⇑g ∘ f) L) = g (List.prod (List.map f L))

theorem List.sum_isAddUnit {M : Type u_3} [AddMonoid M] {L : List M} : (∀ (m : M), m ∈ L → IsAddUnit m) → IsAddUnit (List.sum L)

abbrev List.sum_isAddUnit.match_1 {M : Type u_1} [AddMonoid M] (motive : (x : List M) → (∀ (m : M), m ∈ x → IsAddUnit m) → Prop) : ∀ (x : List M) (x_1 : ∀ (m : M), m ∈ x → IsAddUnit m), (∀ (x : ∀ (m : M), m ∈ [] → IsAddUnit m), motive [] x) → (∀ (h : M) (t : List M) (u : ∀ (m : M), m ∈ h :: t → IsAddUnit m), motive (h :: t) u) → motive x x_1

Equations

• ⋯ = ⋯

theorem List.prod_isUnit {M : Type u_3} [Monoid M] {L : List M} : (∀ (m : M), m ∈ L → IsUnit m) → IsUnit (List.prod L)

theorem List.sum_isAddUnit_iff {α : Type u_9} [AddCommMonoid α] {L : List α} : IsAddUnit (List.sum L) ↔ ∀ (m : α), m ∈ L → IsAddUnit m

theorem List.prod_isUnit_iff {α : Type u_9} [CommMonoid α] {L : List α} : IsUnit (List.prod L) ↔ ∀ (m : α), m ∈ L → IsUnit m

@[simp]

theorem List.sum_take_add_sum_drop {M : Type u_3} [AddMonoid M] (L : List M) (i : ℕ) : List.sum (List.take i L) + List.sum (List.drop i L) = List.sum L

abbrev List.sum_take_add_sum_drop.match_1 {M : Type u_1} (motive : List M → ℕ → Prop) : ∀ (x : List M) (x_1 : ℕ), (∀ (i : ℕ), motive [] i) → (∀ (L : List M), motive L 0) → (∀ (h : M) (t : List M) (n : ℕ), motive (h :: t) (Nat.succ n)) → motive x x_1

Equations

• ⋯ = ⋯

@[simp]

theorem List.prod_take_mul_prod_drop {M : Type u_3} [Monoid M] (L : List M) (i : ℕ) : List.prod (List.take i L) * List.prod (List.drop i L) = List.prod L

@[simp]

theorem List.sum_take_succ {M : Type u_3} [AddMonoid M] (L : List M) (i : ℕ) (p : i < List.length L) : List.sum (List.take (i + 1) L) = List.sum (List.take i L) + List.get L { val := i, isLt := p }

abbrev List.sum_take_succ.match_1 {M : Type u_1} (motive : (x : List M) → (x_1 : ℕ) → x_1 < List.length x → Prop) : ∀ (x : List M) (x_1 : ℕ) (x_2 : x_1 < List.length x), (∀ (i : ℕ) (p : i < List.length []), motive [] i p) → (∀ (h : M) (t : List M) (x : 0 < List.length (h :: t)), motive (h :: t) 0 x) → (∀ (h : M) (t : List M) (n : ℕ) (p : n + 1 < List.length (h :: t)), motive (h :: t) (Nat.succ n) p) → motive x x_1 x_2

Equations

• ⋯ = ⋯

@[simp]

theorem List.prod_take_succ {M : Type u_3} [Monoid M] (L : List M) (i : ℕ) (p : i < List.length L) : List.prod (List.take (i + 1) L) = List.prod (List.take i L) * List.get L { val := i, isLt := p }

theorem List.length_pos_of_sum_ne_zero {M : Type u_3} [AddMonoid M] (L : List M) (h : List.sum L ≠ 0) : 0 < List.length L

A list with sum not zero must have positive length.

theorem List.length_pos_of_prod_ne_one {M : Type u_3} [Monoid M] (L : List M) (h : List.prod L ≠ 1) : 0 < List.length L

A list with product not one must have positive length.

theorem List.length_pos_of_sum_pos {M : Type u_3} [AddMonoid M] [Preorder M] (L : List M) (h : 0 < List.sum L) : 0 < List.length L

A list with positive sum must have positive length.

theorem List.length_pos_of_one_lt_prod {M : Type u_3} [Monoid M] [Preorder M] (L : List M) (h : 1 < List.prod L) : 0 < List.length L

A list with product greater than one must have positive length.

theorem List.length_pos_of_sum_neg {M : Type u_3} [AddMonoid M] [Preorder M] (L : List M) (h : List.sum L < 0) : 0 < List.length L

A list with negative sum must have positive length.

theorem List.length_pos_of_prod_lt_one {M : Type u_3} [Monoid M] [Preorder M] (L : List M) (h : List.prod L < 1) : 0 < List.length L

A list with product less than one must have positive length.

abbrev List.sum_set.match_1 {M : Type u_1} (motive : List M → ℕ → M → Prop) : ∀ (x : List M) (x_1 : ℕ) (x_2 : M), (∀ (x : M) (xs : List M) (a : M), motive (x :: xs) 0 a) → (∀ (x : M) (xs : List M) (i : ℕ) (a : M), motive (x :: xs) (Nat.succ i) a) → (∀ (x : ℕ) (x_3 : M), motive [] x x_3) → motive x x_1 x_2

Equations

• ⋯ = ⋯

theorem List.sum_set {M : Type u_3} [AddMonoid M] (L : List M) (n : ℕ) (a : M) : List.sum (List.set L n a) = (List.sum (List.take n L) + if n < List.length L then a else 0) + List.sum (List.drop (n + 1) L)

theorem List.prod_set {M : Type u_3} [Monoid M] (L : List M) (n : ℕ) (a : M) : List.prod (List.set L n a) = (List.prod (List.take n L) * if n < List.length L then a else 1) * List.prod (List.drop (n + 1) L)

theorem List.get?_zero_add_tail_sum {M : Type u_3} [AddMonoid M] (l : List M) : Option.getD (List.get? l 0) 0 + List.sum (List.tail l) = List.sum l

We'd like to state this as L.headI + L.tail.sum = L.sum, but because L.headI 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.get? 0).getD 0.

theorem List.get?_zero_mul_tail_prod {M : Type u_3} [Monoid M] (l : List M) : Option.getD (List.get? l 0) 1 * List.prod (List.tail l) = List.prod l

We'd like to state this as L.headI * L.tail.prod = L.prod, but because L.headI 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.get? 0).getD 1.

theorem List.headI_add_tail_sum_of_ne_nil {M : Type u_3} [AddMonoid M] [Inhabited M] (l : List M) (h : l ≠ []) : List.headI l + List.sum (List.tail l) = List.sum l

Same as get?_zero_add_tail_sum, but avoiding the List.headI garbage complication by requiring the list to be nonempty.

theorem List.headI_mul_tail_prod_of_ne_nil {M : Type u_3} [Monoid M] [Inhabited M] (l : List M) (h : l ≠ []) : List.headI l * List.prod (List.tail l) = List.prod l

Same as get?_zero_mul_tail_prod, but avoiding the List.headI garbage complication by requiring the list to be nonempty.

theorem AddCommute.list_sum_right {M : Type u_3} [AddMonoid M] (l : List M) (y : M) (h : ∀ (x : M), x ∈ l → AddCommute y x) : AddCommute y (List.sum l)

theorem Commute.list_prod_right {M : Type u_3} [Monoid M] (l : List M) (y : M) (h : ∀ (x : M), x ∈ l → Commute y x) : Commute y (List.prod l)

theorem AddCommute.list_sum_left {M : Type u_3} [AddMonoid M] (l : List M) (y : M) (h : ∀ (x : M), x ∈ l → AddCommute x y) : AddCommute (List.sum l) y

theorem Commute.list_prod_left {M : Type u_3} [Monoid M] (l : List M) (y : M) (h : ∀ (x : M), x ∈ l → Commute x y) : Commute (List.prod l) y

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₂) : List.sum l₁ ≤ List.sum l₂

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₂) : List.prod l₁ ≤ List.prod l₂

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 : List.Sublist l₁ l₂) (h₁ : ∀ (a : M), a ∈ l₂ → 0 ≤ a) : List.sum l₁ ≤ List.sum l₂

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 : List.Sublist l₁ l₂) (h₁ : ∀ (a : M), a ∈ l₂ → 1 ≤ a) : List.prod l₁ ≤ List.prod l₂

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 ∧ List.Sublist l l₂) → Prop) : ∀ (x : ∃ (l : List M), List.Forall₂ (fun (x x_1 : M) => x ≤ x_1) l₁ l ∧ List.Sublist l l₂), (∀ (w : List M) (hall : List.Forall₂ (fun (x x_1 : M) => x ≤ x_1) l₁ w) (hsub : List.Sublist w 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 : M), a ∈ l₂ → 0 ≤ a) : List.sum l₁ ≤ List.sum l₂

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 : M), a ∈ l₂ → 1 ≤ a) : List.prod l₁ ≤ List.prod l₂

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 : ι), i ∈ l → f i ≤ g i) : List.sum (List.map f l) ≤ List.sum (List.map g l)

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 : ι), i ∈ l → f i ≤ g i) : List.prod (List.map f l) ≤ List.prod (List.map g l)

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 : ι), i ∈ l → f i ≤ g i) (h₂ : ∃ (i : ι), i ∈ l ∧ f i < g i) : List.sum (List.map f l) < List.sum (List.map g l)

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 : ι), i ∈ l → f i ≤ g i) (h₂ : ∃ (i : ι), i ∈ l ∧ f i < g i) : List.prod (List.map f l) < List.prod (List.map g l)

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 : ι), i ∈ l → f i < g i) : List.sum (List.map f l) < List.sum (List.map g l)

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 : ι), i ∈ l → f i < g i) : List.prod (List.map f l) < List.prod (List.map g l)

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 : M), x ∈ l → x ≤ n) : List.sum l ≤ List.length l • 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 : M), x ∈ l → x ≤ n) : List.prod l ≤ n ^ List.length l

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.sum (List.map f l) < List.sum (List.map g l)) : ∃ (i : ι), 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.prod (List.map f l) < List.prod (List.map g l)) : ∃ (i : ι), 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.sum (List.map f l) ≤ List.sum (List.map g l)) : ∃ (x : ι), 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.prod (List.map f l) ≤ List.prod (List.map g l)) : ∃ (x : ι), 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 : M), x ∈ l → 0 ≤ x) : 0 ≤ List.sum l

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 : M), x ∈ l → 1 ≤ x) : 1 ≤ List.prod l

theorem List.prod_eq_zero {M₀ : Type u_6} [MonoidWithZero M₀] {L : List M₀} (h : 0 ∈ L) : List.prod L = 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.

@[simp]

theorem List.prod_eq_zero_iff {M₀ : Type u_6} [MonoidWithZero M₀] [Nontrivial M₀] [NoZeroDivisors M₀] {L : List M₀} : List.prod L = 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.

theorem List.prod_ne_zero {M₀ : Type u_6} [MonoidWithZero M₀] [Nontrivial M₀] [NoZeroDivisors M₀] {L : List M₀} (hL : ¬0 ∈ L) : List.prod L ≠ 0

theorem List.sum_neg_reverse {G : Type u_7} [AddGroup G] (L : List G) : -List.sum L = List.sum (List.reverse (List.map (fun (x : G) => -x) L))

This is the List.sum version of add_neg_rev

theorem List.prod_inv_reverse {G : Type u_7} [Group G] (L : List G) : (List.prod L)⁻¹ = List.prod (List.reverse (List.map (fun (x : G) => x⁻¹) L))

This is the List.prod version of mul_inv_rev

theorem List.sum_reverse_noncomm {G : Type u_7} [AddGroup G] (L : List G) : List.sum (List.reverse L) = -List.sum (List.map (fun (x : G) => -x) L)

A non-commutative variant of List.sum_reverse

theorem List.prod_reverse_noncomm {G : Type u_7} [Group G] (L : List G) : List.prod (List.reverse L) = (List.prod (List.map (fun (x : G) => x⁻¹) L))⁻¹

A non-commutative variant of List.prod_reverse

@[simp]

theorem List.sum_drop_succ {G : Type u_7} [AddGroup G] (L : List G) (i : ℕ) (p : i < List.length L) : List.sum (List.drop (i + 1) L) = -List.get L { val := i, isLt := p } + List.sum (List.drop i L)

Counterpart to List.sum_take_succ when we have a negation operation

@[simp]

theorem List.prod_drop_succ {G : Type u_7} [Group G] (L : List G) (i : ℕ) (p : i < List.length L) : List.prod (List.drop (i + 1) L) = (List.get L { val := i, isLt := p })⁻¹ * List.prod (List.drop i L)

Counterpart to List.prod_take_succ when we have an inverse operation

theorem List.sum_range_sub' {G : Type u_7} [AddGroup G] (n : ℕ) (f : ℕ → G) : List.sum (List.map (fun (k : ℕ) => f k - f (k + 1)) (List.range n)) = f 0 - f n

Cancellation of a telescoping sum.

theorem List.prod_range_div' {G : Type u_7} [Group G] (n : ℕ) (f : ℕ → G) : List.prod (List.map (fun (k : ℕ) => f k / f (k + 1)) (List.range n)) = f 0 / f n

Cancellation of a telescoping product.

theorem List.sum_neg {G : Type u_7} [AddCommGroup G] (L : List G) : -List.sum L = List.sum (List.map (fun (x : G) => -x) L)

This is the List.sum version of add_neg

theorem List.prod_inv {G : Type u_7} [CommGroup G] (L : List G) : (List.prod L)⁻¹ = List.prod (List.map (fun (x : G) => x⁻¹) L)

This is the List.prod version of mul_inv

theorem List.sum_range_sub {G : Type u_7} [AddCommGroup G] (n : ℕ) (f : ℕ → G) : List.sum (List.map (fun (k : ℕ) => f (k + 1) - f k) (List.range n)) = f n - f 0

Cancellation of a telescoping sum.

theorem List.prod_range_div {G : Type u_7} [CommGroup G] (n : ℕ) (f : ℕ → G) : List.prod (List.map (fun (k : ℕ) => f (k + 1) / f k) (List.range n)) = f n / f 0

Cancellation of a telescoping product.

theorem List.sum_set' {G : Type u_7} [AddCommGroup G] (L : List G) (n : ℕ) (a : G) : List.sum (List.set L n a) = List.sum L + if hn : n < List.length L then -List.get L { val := n, isLt := hn } + a else 0

Alternative version of List.sum_set when the list is over a group

theorem List.prod_set' {G : Type u_7} [CommGroup G] (L : List G) (n : ℕ) (a : G) : List.prod (List.set L n a) = List.prod L * if hn : n < List.length L then (List.get L { val := n, isLt := hn })⁻¹ * a else 1

Alternative version of List.prod_set when the list is over a group

theorem List.eq_of_sum_take_eq {M : Type u_3} [AddLeftCancelMonoid M] {L : List M} {L' : List M} (h : List.length L = List.length L') (h' : ∀ (i : ℕ), i ≤ List.length L → List.sum (List.take i L) = List.sum (List.take i L')) : L = L'

theorem List.eq_of_prod_take_eq {M : Type u_3} [LeftCancelMonoid M] {L : List M} {L' : List M} (h : List.length L = List.length L') (h' : ∀ (i : ℕ), i ≤ List.length L → List.prod (List.take i L) = List.prod (List.take i L')) : L = L'

theorem List.monotone_sum_take {M : Type u_3} [CanonicallyOrderedAddCommMonoid M] (L : List M) : Monotone fun (i : ℕ) => List.sum (List.take i L)

theorem List.monotone_prod_take {M : Type u_3} [CanonicallyOrderedCommMonoid M] (L : List M) : Monotone fun (i : ℕ) => List.prod (List.take i L)

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

abbrev List.sum_pos.match_1 {M : Type u_1} [OrderedAddCommMonoid M] (motive : (x : List M) → (∀ (x_1 : M), x_1 ∈ x → 0 < x_1) → x ≠ [] → Prop) : ∀ (x : List M) (x_1 : ∀ (x_1 : M), x_1 ∈ x → 0 < x_1) (x_2 : x ≠ []), (∀ (x : ∀ (x : M), x ∈ [] → 0 < x) (h : [] ≠ []), motive [] x h) → (∀ (b : M) (h : ∀ (x : M), x ∈ [b] → 0 < x) (x : [b] ≠ []), motive [b] h x) → (∀ (a b : M) (l : List M) (hl₁ : ∀ (x : M), 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.one_lt_prod_of_one_lt {M : Type u_3} [OrderedCommMonoid M] (l : List M) : (∀ (x : M), x ∈ l → 1 < x) → l ≠ [] → 1 < List.prod l

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

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

theorem List.all_zero_of_le_zero_le_of_sum_eq_zero {M : Type u_3} [OrderedAddCommMonoid M] {l : List M} (hl₁ : ∀ (x : M), x ∈ l → 0 ≤ x) (hl₂ : List.sum l = 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 : M), x ∈ l → 1 ≤ x) (hl₂ : List.prod l = 1) {x : M} (hx : x ∈ l) : x = 1

theorem List.sum_eq_zero {M : Type u_3} [AddMonoid M] {l : List M} (hl : ∀ (x : M), x ∈ l → x = 0) : List.sum l = 0

Slightly more general version of List.sum_eq_zero_iff for a non-ordered AddMonoid

theorem List.prod_eq_one {M : Type u_3} [Monoid M] {l : List M} (hl : ∀ (x : M), x ∈ l → x = 1) : List.prod l = 1

Slightly more general version of List.prod_eq_one_iff for a non-ordered Monoid

theorem List.exists_mem_ne_zero_of_sum_ne_zero {M : Type u_3} [AddMonoid M] {l : List M} (h : List.sum l ≠ 0) : ∃ (x : M), x ∈ l ∧ x ≠ 0

theorem List.exists_mem_ne_one_of_prod_ne_one {M : Type u_3} [Monoid M] {l : List M} (h : List.prod l ≠ 1) : ∃ (x : M), x ∈ l ∧ x ≠ 1

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 (List.sum l) ≤ List.foldr max 0 (List.map f l)

theorem List.sum_erase_of_comm {M : Type u_3} [DecidableEq M] [AddMonoid M] {a : M} {l : List M} (ha : a ∈ l) (comm : ∀ (x : M), x ∈ l → ∀ (y : M), y ∈ l → x + y = y + x) : a + List.sum (List.erase l a) = List.sum l

theorem List.prod_erase_of_comm {M : Type u_3} [DecidableEq M] [Monoid M] {a : M} {l : List M} (ha : a ∈ l) (comm : ∀ (x : M), x ∈ l → ∀ (y : M), y ∈ l → x * y = y * x) : a * List.prod (List.erase l a) = List.prod l

@[simp]

theorem List.sum_erase {M : Type u_3} [DecidableEq M] [AddCommMonoid M] {a : M} {l : List M} (ha : a ∈ l) : a + List.sum (List.erase l a) = List.sum l

@[simp]

theorem List.prod_erase {M : Type u_3} [DecidableEq M] [CommMonoid M] {a : M} {l : List M} (ha : a ∈ l) : a * List.prod (List.erase l a) = List.prod l

abbrev List.sum_map_erase.match_1 {ι : Type u_1} {a : ι} (motive : (x : List ι) → a ∈ x → Prop) : ∀ (x : List ι) (x_1 : a ∈ x), (∀ (b : ι) (l : List ι) (h : a ∈ b :: l), motive (b :: l) h) → motive x x_1

Equations

• ⋯ = ⋯

@[simp]

theorem List.sum_map_erase {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [AddCommMonoid M] (f : ι → M) {a : ι} {l : List ι} : a ∈ l → f a + List.sum (List.map f (List.erase l a)) = List.sum (List.map f l)

@[simp]

theorem List.prod_map_erase {ι : Type u_1} {M : Type u_3} [DecidableEq ι] [CommMonoid M] (f : ι → M) {a : ι} {l : List ι} : a ∈ l → f a * List.prod (List.map f (List.erase l a)) = List.prod (List.map f l)

theorem List.sum_const_nat (m : ℕ) (n : ℕ) : List.sum (List.replicate m n) = m * n

theorem List.prod_pos {R : Type u_8} [StrictOrderedSemiring R] (l : List R) (h : ∀ (a : R), a ∈ l → 0 < a) : 0 < List.prod l

The product of a list of positive natural numbers is positive, and likewise for any nontrivial ordered semiring.

@[simp]

theorem CanonicallyOrderedCommSemiring.list_prod_pos {α : Type u_9} [CanonicallyOrderedCommSemiring α] [Nontrivial α] {l : List α} : 0 < List.prod l ↔ ∀ (x : α), x ∈ l → 0 < x

A variant of List.prod_pos for CanonicallyOrderedCommSemiring.

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.

theorem List.headI_add_tail_sum (L : List ℕ) : List.headI L + List.sum (List.tail L) = List.sum L

This relies on default ℕ = 0.

theorem List.headI_le_sum (L : List ℕ) : List.headI L ≤ List.sum L

This relies on default ℕ = 0.

theorem List.tail_sum (L : List ℕ) : List.sum (List.tail L) = List.sum L - List.headI L

This relies on default ℕ = 0.

@[simp]

theorem List.alternatingSum_nil {α : Type u_2} [Zero α] [Add α] [Neg α] : List.alternatingSum [] = 0

@[simp]

theorem List.alternatingProd_nil {α : Type u_2} [One α] [Mul α] [Inv α] : List.alternatingProd [] = 1

@[simp]

theorem List.alternatingSum_singleton {α : Type u_2} [Zero α] [Add α] [Neg α] (a : α) : List.alternatingSum [a] = a

@[simp]

theorem List.alternatingProd_singleton {α : Type u_2} [One α] [Mul α] [Inv α] (a : α) : List.alternatingProd [a] = a

theorem List.alternatingSum_cons_cons' {α : Type u_2} [Zero α] [Add α] [Neg α] (a : α) (b : α) (l : List α) : List.alternatingSum (a :: b :: l) = a + -b + List.alternatingSum l

theorem List.alternatingProd_cons_cons' {α : Type u_2} [One α] [Mul α] [Inv α] (a : α) (b : α) (l : List α) : List.alternatingProd (a :: b :: l) = a * b⁻¹ * List.alternatingProd l

theorem List.alternatingSum_cons_cons {α : Type u_2} [SubNegMonoid α] (a : α) (b : α) (l : List α) : List.alternatingSum (a :: b :: l) = a - b + List.alternatingSum l

theorem List.alternatingProd_cons_cons {α : Type u_2} [DivInvMonoid α] (a : α) (b : α) (l : List α) : List.alternatingProd (a :: b :: l) = a / b * List.alternatingProd l

theorem List.alternatingSum_cons' {α : Type u_2} [AddCommGroup α] (a : α) (l : List α) : List.alternatingSum (a :: l) = a + -List.alternatingSum l

abbrev List.alternatingSum_cons'.match_1 {α : Type u_1} (motive : α → List α → Prop) : ∀ (x : α) (x_1 : List α), (∀ (a : α), motive a []) → (∀ (a b : α) (l : List α), motive a (b :: l)) → motive x x_1

Equations

• ⋯ = ⋯

theorem List.alternatingProd_cons' {α : Type u_2} [CommGroup α] (a : α) (l : List α) : List.alternatingProd (a :: l) = a * (List.alternatingProd l)⁻¹

@[simp]

theorem List.alternatingSum_cons {α : Type u_2} [AddCommGroup α] (a : α) (l : List α) : List.alternatingSum (a :: l) = a - List.alternatingSum l

@[simp]

theorem List.alternatingProd_cons {α : Type u_2} [CommGroup α] (a : α) (l : List α) : List.alternatingProd (a :: l) = a / List.alternatingProd l

theorem List.sum_nat_mod (l : List ℕ) (n : ℕ) : List.sum l % n = List.sum (List.map (fun (x : ℕ) => x % n) l) % n

theorem List.prod_nat_mod (l : List ℕ) (n : ℕ) : List.prod l % n = List.prod (List.map (fun (x : ℕ) => x % n) l) % n

theorem List.sum_int_mod (l : List ℤ) (n : ℤ) : List.sum l % n = List.sum (List.map (fun (x : ℤ) => x % n) l) % n

theorem List.prod_int_mod (l : List ℤ) (n : ℤ) : List.prod l % n = List.prod (List.map (fun (x : ℤ) => x % n) l) % n

theorem map_list_sum {M : Type u_3} {N : Type u_4} [AddMonoid M] [AddMonoid N] {F : Type u_9} [FunLike F M N] [AddMonoidHomClass F M N] (f : F) (l : List M) : f (List.sum l) = List.sum (List.map (⇑f) l)

theorem map_list_prod {M : Type u_3} {N : Type u_4} [Monoid M] [Monoid N] {F : Type u_9} [FunLike F M N] [MonoidHomClass F M N] (f : F) (l : List M) : f (List.prod l) = List.prod (List.map (⇑f) l)

theorem AddMonoidHom.map_list_sum {M : Type u_3} {N : Type u_4} [AddMonoid M] [AddMonoid N] (f : M →+ N) (l : List M) : f (List.sum l) = List.sum (List.map (⇑f) l)

Deprecated, use _root_.map_list_sum instead.

theorem MonoidHom.map_list_prod {M : Type u_3} {N : Type u_4} [Monoid M] [Monoid N] (f : M →* N) (l : List M) : f (List.prod l) = List.prod (List.map (⇑f) l)

Deprecated, use _root_.map_list_prod instead.