feat: lemmas about sums of lists/arrays/vectors

src/Init/Data/Array.lean

@@ -31,3 +31,5 @@ public import Init.Data.Array.Zip
 public import Init.Data.Array.InsertIdx
 public import Init.Data.Array.Extract
 public import Init.Data.Array.MinMax
+public import Init.Data.Array.Nat
+public import Init.Data.Array.Int

src/Init/Data/Array/Find.lean

@@ -7,6 +7,7 @@ module
 
 prelude
 public import Init.Data.List.Nat.Find
+import Init.Data.List.Nat.Sum
 import all Init.Data.Array.Basic
 public import Init.Data.Array.Range
 
@@ -114,7 +115,7 @@ theorem getElem_zero_flatten.proof {xss : Array (Array α)} (h : 0 < xss.flatten
   simp only [List.findSome?_toArray, List.findSome?_map, Function.comp_def, List.getElem?_toArray,
     List.findSome?_isSome_iff, isSome_getElem?]
   simp only [flatten_toArray_map_toArray, List.size_toArray, List.length_flatten,
-    Nat.sum_pos_iff_exists_pos, List.mem_map] at h
+    List.sum_pos_iff_exists_pos_nat, List.mem_map] at h
   obtain ⟨_, ⟨xs, m, rfl⟩, h⟩ := h
   exact ⟨xs, m, by simpa using h⟩
 

src/Init/Data/Array/Int.lean

@@ -0,0 +1,35 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison, Sebastian Graf, Paul Reichert
+-/
+module
+
+prelude
+public import Init.Data.List.Int.Sum
+public import Init.Data.Array.Lemmas
+public import Init.Data.Int.DivMod.Bootstrap
+import Init.Data.Int.DivMod.Lemmas
+import Init.Data.List.MinMax
+
+public section
+
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+
+namespace Array
+
+@[simp] theorem sum_replicate_int {n : Nat} {a : Int} : (replicate n a).sum = n * a := by
+  rw [← List.toArray_replicate, List.sum_toArray]
+  simp
+
+theorem sum_append_int {as₁ as₂ : Array Int} : (as₁ ++ as₂).sum = as₁.sum + as₂.sum := by
+  simp [sum_append]
+
+theorem sum_reverse_int (xs : Array Int) : xs.reverse.sum = xs.sum := by
+  simp [sum_reverse]
+
+theorem sum_eq_foldl_int {xs : Array Int} : xs.sum = xs.foldl (init := 0) (· + ·) := by
+  simp only [foldl_eq_foldr_reverse, Int.add_comm, ← sum_eq_foldr, sum_reverse_int]
+
+end Array

src/Init/Data/Array/Lemmas.lean

@@ -2509,10 +2509,6 @@ theorem flatMap_replicate {f : α → Array β} : (replicate n a).flatMap f = (r
   rw [← List.toArray_replicate, List.isEmpty_toArray]
   simp
 
-@[simp] theorem sum_replicate_nat {n : Nat} {a : Nat} : (replicate n a).sum = n * a := by
-  rw [← List.toArray_replicate, List.sum_toArray]
-  simp
-
 /-! ### Preliminaries about `swap` needed for `reverse`. -/
 
 @[grind =]
@@ -4298,19 +4294,31 @@ theorem getElem?_range {n : Nat} {i : Nat} : (Array.range n)[i]? = if i < n then
 /-! ### sum -/
 
 @[simp, grind =] theorem sum_empty [Add α] [Zero α] : (#[] : Array α).sum = 0 := rfl
+theorem sum_eq_foldr [Add α] [Zero α] {xs : Array α} :
+    xs.sum = xs.foldr (init := 0) (· + ·) :=
+  rfl
 
 -- Without further algebraic hypotheses, there's no useful `sum_push` lemma.
 
 @[simp, grind =]
-theorem sum_eq_sum_toList [Add α] [Zero α] {as : Array α} : as.toList.sum = as.sum := by
+theorem sum_toList [Add α] [Zero α] {as : Array α} : as.toList.sum = as.sum := by
   cases as
   simp [Array.sum, List.sum]
 
+@[deprecated sum_toList (since := "2026-01-14")]
+def sum_eq_sum_toList := @sum_toList
+
+@[simp, grind =]
+theorem sum_append [Zero α] [Add α] [Std.Associative (α := α) (· + ·)]
+    [Std.LeftIdentity (α := α) (· + ·) 0] [Std.LawfulLeftIdentity (α := α) (· + ·) 0]
+    {as₁ as₂ : Array α} : (as₁ ++ as₂).sum = as₁.sum + as₂.sum := by
+  simp [← sum_toList, List.sum_append]
+
 @[simp, grind =]
-theorem sum_append_nat {as₁ as₂ : Array Nat} : (as₁ ++ as₂).sum = as₁.sum + as₂.sum := by
-  cases as₁
-  cases as₂
-  simp [List.sum_append_nat]
+theorem sum_reverse [Zero α] [Add α] [Std.Associative (α := α) (· + ·)]
+    [Std.Commutative (α := α) (· + ·)]
+    [Std.LawfulLeftIdentity (α := α) (· + ·) 0] (xs : Array α) : xs.reverse.sum = xs.sum := by
+  simp [← sum_toList, List.sum_reverse]
 
 theorem foldl_toList_eq_flatMap {l : List α} {acc : Array β}
     {F : Array β → α → Array β} {G : α → List β}

src/Init/Data/Array/Nat.lean

@@ -0,0 +1,39 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison, Sebastian Graf, Paul Reichert
+-/
+module
+
+prelude
+public import Init.Data.Array.Lemmas
+import Init.Data.List.Nat.Sum
+
+public section
+
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+
+namespace Array
+
+protected theorem sum_pos_iff_exists_pos_nat {xs : Array Nat} : 0 < xs.sum ↔ ∃ x ∈ xs, 0 < x := by
+  simp [← sum_toList, List.sum_pos_iff_exists_pos_nat]
+
+protected theorem sum_eq_zero_iff_forall_eq_nat {xs : Array Nat} :
+    xs.sum = 0 ↔ ∀ x ∈ xs, x = 0 := by
+  simp [← sum_toList, List.sum_eq_zero_iff_forall_eq_nat]
+
+@[simp] theorem sum_replicate_nat {n : Nat} {a : Nat} : (replicate n a).sum = n * a := by
+  rw [← List.toArray_replicate, List.sum_toArray]
+  simp
+
+theorem sum_append_nat {as₁ as₂ : Array Nat} : (as₁ ++ as₂).sum = as₁.sum + as₂.sum := by
+  simp [sum_append]
+
+theorem sum_reverse_nat (xs : Array Nat) : xs.reverse.sum = xs.sum := by
+  simp [sum_reverse]
+
+theorem sum_eq_foldl_nat {xs : Array Nat} : xs.sum = xs.foldl (init := 0) (· + ·) := by
+  simp only [foldl_eq_foldr_reverse, Nat.add_comm, ← sum_eq_foldr, sum_reverse_nat]
+
+end Array

src/Init/Data/List.lean

@@ -20,6 +20,7 @@ public import Init.Data.List.MinMaxIdx
 public import Init.Data.List.MinMaxOn
 public import Init.Data.List.Monadic
 public import Init.Data.List.Nat
+public import Init.Data.List.Int
 public import Init.Data.List.Notation
 public import Init.Data.List.Pairwise
 public import Init.Data.List.Sublist

src/Init/Data/List/Basic.lean

@@ -2017,6 +2017,7 @@ def sum {α} [Add α] [Zero α] : List α → α :=
 
 @[simp, grind =] theorem sum_nil [Add α] [Zero α] : ([] : List α).sum = 0 := rfl
 @[simp, grind =] theorem sum_cons [Add α] [Zero α] {a : α} {l : List α} : (a::l).sum = a + l.sum := rfl
+theorem sum_eq_foldr [Add α] [Zero α] {l : List α} : l.sum = l.foldr (· + ·) 0 := rfl
 
 /-! ### range -/
 

src/Init/Data/List/Int.lean

@@ -0,0 +1,9 @@
+/-
+Copyright (c) 2026 Lean FRO. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Paul Reichert
+-/
+module
+
+prelude
+public import Init.Data.List.Int.Sum

src/Init/Data/List/Int/Sum.lean

@@ -0,0 +1,107 @@
+/-
+Copyright (c) 2026 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison, Sebastian Graf, Paul Reichert
+-/
+module
+
+prelude
+public import Init.Data.Int.DivMod.Bootstrap
+import Init.Data.Int.DivMod.Lemmas
+import Init.Data.List.MinMax
+
+public section
+
+set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
+set_option linter.indexVariables true -- Enforce naming conventions for index variables.
+
+namespace List
+
+@[simp]
+theorem sum_replicate_int {n : Nat} {a : Int} : (replicate n a).sum = n * a := by
+  induction n <;> simp_all [replicate_succ, Int.add_mul, Int.add_comm]
+
+theorem sum_append_int {l₁ l₂ : List Int} : (l₁ ++ l₂).sum = l₁.sum + l₂.sum := by
+  simp [sum_append]
+
+theorem sum_reverse_int (xs : List Int) : xs.reverse.sum = xs.sum := by
+  simp [sum_reverse]
+
+theorem min_mul_length_le_sum_int {xs : List Int} (h : xs ≠ []) :
+    xs.min h * xs.length ≤ xs.sum := by
+  induction xs
+  · contradiction
+  · rename_i x xs ih
+    cases xs
+    · simp_all [List.min_singleton]
+    · simp only [ne_eq, reduceCtorEq, not_false_eq_true, min_eq_get_min?,
+      List.min?_cons (α := Int), Option.get_some, length_cons, Int.natCast_add, Int.cast_ofNat_Int,
+      forall_const] at ih ⊢
+      rw [Int.mul_add, Int.mul_one, Int.add_comm]
+      apply Int.add_le_add
+      · apply Int.min_le_left
+      · refine Int.le_trans ?_ ih
+        rw [Int.mul_le_mul_right (by omega)]
+        apply Int.min_le_right
+
+theorem mul_length_le_sum_of_min?_eq_some_int {xs : List Int} (h : xs.min? = some x) :
+    x * xs.length ≤ xs.sum := by
+  cases xs
+  · simp_all
+  · simp only [min?_eq_some_min (cons_ne_nil _ _), Option.some.injEq] at h
+    simpa [← h] using min_mul_length_le_sum_int _
+
+theorem min_le_sum_div_length_int {xs : List Int} (h : xs ≠ []) :
+    xs.min h ≤ xs.sum / xs.length := by
+  have := min_mul_length_le_sum_int h
+  rwa [Int.le_ediv_iff_mul_le]
+  simp [List.length_pos_iff, h]
+
+theorem le_sum_div_length_of_min?_eq_some_int {xs : List Int} (h : xs.min? = some x) :
+    x ≤ xs.sum / xs.length := by
+  cases xs
+  · simp_all
+  · simp only [min?_eq_some_min (cons_ne_nil _ _), Option.some.injEq] at h
+    simpa [← h] using min_le_sum_div_length_int _
+
+theorem sum_le_max_mul_length_int {xs : List Int} (h : xs ≠ []) :
+    xs.sum ≤ xs.max h * xs.length := by
+  induction xs
+  · contradiction
+  · rename_i x xs ih
+    cases xs
+    · simp_all [List.max_singleton]
+    · simp only [ne_eq, reduceCtorEq, not_false_eq_true, max_eq_get_max?,
+      List.max?_cons (α := Int), Option.get_some, length_cons, Int.natCast_add, Int.cast_ofNat_Int,
+      forall_const] at ih ⊢
+      rw [Int.mul_add, Int.mul_one, Int.add_comm]
+      apply Int.add_le_add
+      · apply Int.le_max_left
+      · refine Int.le_trans ih ?_
+        rw [Int.mul_le_mul_right (by omega)]
+        apply Int.le_max_right
+
+theorem sum_le_max_mul_length_of_max?_eq_some_int {xs : List Int} (h : xs.max? = some x) :
+    xs.sum ≤ x * xs.length := by
+  cases xs
+  · simp_all
+  · simp only [max?_eq_some_max (cons_ne_nil _ _), Option.some.injEq] at h
+    simpa [← h] using sum_le_max_mul_length_int _
+
+theorem sum_div_length_le_max_int {xs : List Int} (h : xs ≠ []) :
+    xs.sum / xs.length ≤ xs.max h := by
+  have := sum_le_max_mul_length_int h
+  rw [Int.ediv_le_iff_le_mul]
+  · refine Int.lt_of_le_of_lt this ?_
+    apply Int.lt_add_of_pos_right
+    simp [← Nat.ne_zero_iff_zero_lt, h]
+  · simp [List.length_pos_iff, h]
+
+theorem sum_div_length_le_max_of_max?_eq_some_int {xs : List Int} (h : xs.max? = some x) :
+    xs.sum / xs.length ≤ x := by
+  cases xs
+  · simp_all
+  · simp only [max?_eq_some_max (cons_ne_nil _ _), Option.some.injEq] at h
+    simpa [← h] using sum_div_length_le_max_int _
+
+end List

src/Init/Data/List/Lemmas.lean

@@ -1830,12 +1830,17 @@ theorem append_eq_map_iff {f : α → β} :
   rw [eq_comm, map_eq_append_iff]
 
 @[simp, grind =]
-theorem sum_append_nat {l₁ l₂ : List Nat} : (l₁ ++ l₂).sum = l₁.sum + l₂.sum := by
-  induction l₁ generalizing l₂ <;> simp_all [Nat.add_assoc]
+theorem sum_append [Add α] [Zero α] [Std.LawfulLeftIdentity (α := α) (· + ·) 0]
+    [Std.Associative (α := α) (· + ·)] {l₁ l₂ : List α} : (l₁ ++ l₂).sum = l₁.sum + l₂.sum := by
+  induction l₁ generalizing l₂ <;> simp_all [Std.Associative.assoc, Std.LawfulLeftIdentity.left_id]
 
 @[simp, grind =]
-theorem sum_reverse_nat (xs : List Nat) : xs.reverse.sum = xs.sum := by
-  induction xs <;> simp_all [Nat.add_comm]
+theorem sum_reverse [Zero α] [Add α] [Std.Associative (α := α) (· + ·)]
+    [Std.Commutative (α := α) (· + ·)]
+    [Std.LawfulLeftIdentity (α := α) (· + ·) 0] (xs : List α) : xs.reverse.sum = xs.sum := by
+  induction xs <;>
+    simp_all [sum_append, Std.Commutative.comm (α := α) _ 0,
+      Std.LawfulLeftIdentity.left_id, Std.Commutative.comm]
 
 /-! ### concat
 
@@ -2366,9 +2371,6 @@ theorem replicateRecOn {α : Type _} {p : List α → Prop} (l : List α)
     exact hi _ _ _ _ h hn (replicateRecOn (b :: l') h0 hr hi)
 termination_by l.length
 
-@[simp] theorem sum_replicate_nat {n : Nat} {a : Nat} : (replicate n a).sum = n * a := by
-  induction n <;> simp_all [replicate_succ, Nat.add_mul, Nat.add_comm]
-
 /-! ### reverse -/
 
 @[simp, grind =] theorem length_reverse {as : List α} : (as.reverse).length = as.length := by

src/Init/Data/List/Nat.lean

@@ -12,6 +12,7 @@ public import Init.Data.List.Nat.Range
 public import Init.Data.List.Nat.Sublist
 public import Init.Data.List.Nat.TakeDrop
 public import Init.Data.List.Nat.Count
+public import Init.Data.List.Nat.Sum
 public import Init.Data.List.Nat.Erase
 public import Init.Data.List.Nat.Find
 public import Init.Data.List.Nat.BEq

src/Init/Data/List/Nat/Find.lean

@@ -13,13 +13,6 @@ public section
 set_option linter.listVariables true -- Enforce naming conventions for `List`/`Array`/`Vector` variables.
 set_option linter.indexVariables true -- Enforce naming conventions for index variables.
 
-protected theorem Nat.sum_pos_iff_exists_pos {l : List Nat} : 0 < l.sum ↔ ∃ x ∈ l, 0 < x := by
-  induction l with
-  | nil => simp
-  | cons x xs ih =>
-    simp [← ih]
-    omega
-
 namespace List
 
 open Nat