chore(CauSeq): Cleanup (#10530)

* Rename `Data.Real.CauSeq` to `Algebra.Order.CauSeq.Basic`
* Rename `Data.Real.CauSeqCompletion` to `Algebra.Order.CauSeq.Completion`
* Move the general lemmas about `CauSeq` from `Data.Complex.Exponential` to a new file `Algebra.Order.CauSeq.BigOperators`
* Move the lemmas mentioning `Module` from `Algebra.BigOperators.Intervals` to a new file `Algebra.BigOperators.Module`
* Move a few more lemmas to earlier files
* Deprecate `abv_sum_le_sum_abv` as it's a duplicate of `IsAbsoluteValue.abv_sum`

Mathlib.lean

@@ -26,6 +26,7 @@ import Mathlib.Algebra.BigOperators.Fin
 import Mathlib.Algebra.BigOperators.Finprod
 import Mathlib.Algebra.BigOperators.Finsupp
 import Mathlib.Algebra.BigOperators.Intervals
+import Mathlib.Algebra.BigOperators.Module
 import Mathlib.Algebra.BigOperators.Multiset.Basic
 import Mathlib.Algebra.BigOperators.Multiset.Lemmas
 import Mathlib.Algebra.BigOperators.NatAntidiagonal
@@ -364,6 +365,9 @@ import Mathlib.Algebra.Opposites
 import Mathlib.Algebra.Order.AbsoluteValue
 import Mathlib.Algebra.Order.Algebra
 import Mathlib.Algebra.Order.Archimedean
+import Mathlib.Algebra.Order.CauSeq.Basic
+import Mathlib.Algebra.Order.CauSeq.BigOperators
+import Mathlib.Algebra.Order.CauSeq.Completion
 import Mathlib.Algebra.Order.Chebyshev
 import Mathlib.Algebra.Order.CompleteField
 import Mathlib.Algebra.Order.EuclideanAbsoluteValue
@@ -1989,8 +1993,6 @@ import Mathlib.Data.Rbtree.MinMax
 import Mathlib.Data.Real.Archimedean
 import Mathlib.Data.Real.Basic
 import Mathlib.Data.Real.Cardinality
-import Mathlib.Data.Real.CauSeq
-import Mathlib.Data.Real.CauSeqCompletion
 import Mathlib.Data.Real.ConjugateExponents
 import Mathlib.Data.Real.ENatENNReal
 import Mathlib.Data.Real.EReal

Mathlib/Algebra/BigOperators/Intervals.lean

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl
 -/
 import Mathlib.Algebra.BigOperators.Basic
-import Mathlib.Algebra.Module.Basic
 import Mathlib.Data.Nat.Interval
 import Mathlib.Tactic.Linarith
 
@@ -258,6 +257,19 @@ theorem sum_range_id (n : ℕ) : ∑ i in range n, i = n * (n - 1) / 2 := by
 
 end GaussSum
 
+@[to_additive]
+lemma prod_range_diag_flip (n : ℕ) (f : ℕ → ℕ → M) :
+    (∏ m in range n, ∏ k in range (m + 1), f k (m - k)) =
+      ∏ m in range n, ∏ k in range (n - m), f m k := by
+  rw [prod_sigma', prod_sigma']
+  refine prod_nbij' (fun a ↦ ⟨a.2, a.1 - a.2⟩) (fun a ↦ ⟨a.1 + a.2, a.1⟩) ?_ ?_ ?_ ?_ ?_ <;>
+    simp (config := { contextual := true }) only [mem_sigma, mem_range, lt_tsub_iff_left,
+      Nat.lt_succ_iff, le_add_iff_nonneg_right, Nat.zero_le, and_true, and_imp, imp_self,
+      implies_true, Sigma.forall, forall_const, add_tsub_cancel_of_le, Sigma.mk.inj_iff,
+      add_tsub_cancel_left, heq_eq_eq]
+  · exact fun a b han hba ↦ lt_of_le_of_lt hba han
+#align sum_range_diag_flip Finset.sum_range_diag_flip
+
 end Generic
 
 section Nat
@@ -298,68 +310,4 @@ theorem prod_Ico_succ_div_top (hmn : m ≤ n) :
 end Group
 
 end Nat
-
-section Module
-
-variable {R M : Type*} [Ring R] [AddCommGroup M] [Module R M] (f : ℕ → R) (g : ℕ → M) {m n : ℕ}
-
-open Finset
-
--- The partial sum of `g`, starting from zero
-local notation "G " n:80 => ∑ i in range n, g i
-
-/-- **Summation by parts**, also known as **Abel's lemma** or an **Abel transformation** -/
-theorem sum_Ico_by_parts (hmn : m < n) :
-    ∑ i in Ico m n, f i • g i =
-      f (n - 1) • G n - f m • G m - ∑ i in Ico m (n - 1), (f (i + 1) - f i) • G (i + 1) := by
-  have h₁ : (∑ i in Ico (m + 1) n, f i • G i) = ∑ i in Ico m (n - 1), f (i + 1) • G (i + 1) := by
-    rw [← Nat.sub_add_cancel (Nat.one_le_of_lt hmn), ← sum_Ico_add']
-    simp only [ge_iff_le, tsub_le_iff_right, add_le_iff_nonpos_left, nonpos_iff_eq_zero,
-      tsub_eq_zero_iff_le, add_tsub_cancel_right]
-  have h₂ :
-    (∑ i in Ico (m + 1) n, f i • G (i + 1)) =
-      (∑ i in Ico m (n - 1), f i • G (i + 1)) + f (n - 1) • G n - f m • G (m + 1) := by
-    rw [← sum_Ico_sub_bot _ hmn, ← sum_Ico_succ_sub_top _ (Nat.le_sub_one_of_lt hmn),
-      Nat.sub_add_cancel (pos_of_gt hmn), sub_add_cancel]
-  rw [sum_eq_sum_Ico_succ_bot hmn]
-  -- porting note: the following used to be done with `conv`
-  have h₃: (Finset.sum (Ico (m + 1) n) fun i => f i • g i) =
-             (Finset.sum (Ico (m + 1) n) fun i =>
-                f i • ((Finset.sum (Finset.range (i + 1)) g) -
-                        (Finset.sum (Finset.range i) g))) := by
-    congr; funext; rw [← sum_range_succ_sub_sum g]
-  rw [h₃]
-  simp_rw [smul_sub, sum_sub_distrib, h₂, h₁]
-  -- porting note: the following used to be done with `conv`
-  have h₄ : ((((Finset.sum (Ico m (n - 1)) fun i => f i • Finset.sum (range (i + 1)) fun i => g i) +
-      f (n - 1) • Finset.sum (range n) fun i => g i) -
-      f m • Finset.sum (range (m + 1)) fun i => g i) -
-      Finset.sum (Ico m (n - 1)) fun i => f (i + 1) • Finset.sum (range (i + 1)) fun i => g i) =
-      f (n - 1) • (range n).sum g - f m • (range (m + 1)).sum g +
-      Finset.sum (Ico m (n - 1)) (fun i => f i • (range (i + 1)).sum g -
-      f (i + 1) • (range (i + 1)).sum g) := by
-    rw [← add_sub, add_comm, ← add_sub, ← sum_sub_distrib]
-  rw [h₄]
-  have : ∀ i, f i • G (i + 1) - f (i + 1) • G (i + 1) = -((f (i + 1) - f i) • G (i + 1)) := by
-    intro i
-    rw [sub_smul]
-    abel
-  simp_rw [this, sum_neg_distrib, sum_range_succ, smul_add]
-  abel
-#align finset.sum_Ico_by_parts Finset.sum_Ico_by_parts
-
-variable (n)
-
-/-- **Summation by parts** for ranges -/
-theorem sum_range_by_parts :
-    ∑ i in range n, f i • g i =
-      f (n - 1) • G n - ∑ i in range (n - 1), (f (i + 1) - f i) • G (i + 1) := by
-  by_cases hn : n = 0
-  · simp [hn]
-  · rw [range_eq_Ico, sum_Ico_by_parts f g (Nat.pos_of_ne_zero hn), sum_range_zero, smul_zero,
-      sub_zero, range_eq_Ico]
-#align finset.sum_range_by_parts Finset.sum_range_by_parts
-
-end Module
-
 end Finset

Mathlib/Algebra/BigOperators/Module.lean

@@ -0,0 +1,73 @@
+/-
+Copyright (c) 2022 Dylan MacKenzie. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Dylan MacKenzie
+-/
+import Mathlib.Algebra.BigOperators.Intervals
+import Mathlib.Algebra.Module.Basic
+
+/-!
+# Summation by parts
+-/
+
+open scoped BigOperators
+
+namespace Finset
+variable {R M : Type*} [Ring R] [AddCommGroup M] [Module R M] (f : ℕ → R) (g : ℕ → M) {m n : ℕ}
+
+-- The partial sum of `g`, starting from zero
+local notation "G " n:80 => ∑ i in range n, g i
+
+/-- **Summation by parts**, also known as **Abel's lemma** or an **Abel transformation** -/
+theorem sum_Ico_by_parts (hmn : m < n) :
+    ∑ i in Ico m n, f i • g i =
+      f (n - 1) • G n - f m • G m - ∑ i in Ico m (n - 1), (f (i + 1) - f i) • G (i + 1) := by
+  have h₁ : (∑ i in Ico (m + 1) n, f i • G i) = ∑ i in Ico m (n - 1), f (i + 1) • G (i + 1) := by
+    rw [← Nat.sub_add_cancel (Nat.one_le_of_lt hmn), ← sum_Ico_add']
+    simp only [ge_iff_le, tsub_le_iff_right, add_le_iff_nonpos_left, nonpos_iff_eq_zero,
+      tsub_eq_zero_iff_le, add_tsub_cancel_right]
+  have h₂ :
+    (∑ i in Ico (m + 1) n, f i • G (i + 1)) =
+      (∑ i in Ico m (n - 1), f i • G (i + 1)) + f (n - 1) • G n - f m • G (m + 1) := by
+    rw [← sum_Ico_sub_bot _ hmn, ← sum_Ico_succ_sub_top _ (Nat.le_sub_one_of_lt hmn),
+      Nat.sub_add_cancel (pos_of_gt hmn), sub_add_cancel]
+  rw [sum_eq_sum_Ico_succ_bot hmn]
+  -- porting note: the following used to be done with `conv`
+  have h₃: (Finset.sum (Ico (m + 1) n) fun i => f i • g i) =
+             (Finset.sum (Ico (m + 1) n) fun i =>
+                f i • ((Finset.sum (Finset.range (i + 1)) g) -
+                        (Finset.sum (Finset.range i) g))) := by
+    congr; funext; rw [← sum_range_succ_sub_sum g]
+  rw [h₃]
+  simp_rw [smul_sub, sum_sub_distrib, h₂, h₁]
+  -- porting note: the following used to be done with `conv`
+  have h₄ : ((((Finset.sum (Ico m (n - 1)) fun i => f i • Finset.sum (range (i + 1)) fun i => g i) +
+      f (n - 1) • Finset.sum (range n) fun i => g i) -
+      f m • Finset.sum (range (m + 1)) fun i => g i) -
+      Finset.sum (Ico m (n - 1)) fun i => f (i + 1) • Finset.sum (range (i + 1)) fun i => g i) =
+      f (n - 1) • (range n).sum g - f m • (range (m + 1)).sum g +
+      Finset.sum (Ico m (n - 1)) (fun i => f i • (range (i + 1)).sum g -
+      f (i + 1) • (range (i + 1)).sum g) := by
+    rw [← add_sub, add_comm, ← add_sub, ← sum_sub_distrib]
+  rw [h₄]
+  have : ∀ i, f i • G (i + 1) - f (i + 1) • G (i + 1) = -((f (i + 1) - f i) • G (i + 1)) := by
+    intro i
+    rw [sub_smul]
+    abel
+  simp_rw [this, sum_neg_distrib, sum_range_succ, smul_add]
+  abel
+#align finset.sum_Ico_by_parts Finset.sum_Ico_by_parts
+
+variable (n)
+
+/-- **Summation by parts** for ranges -/
+theorem sum_range_by_parts :
+    ∑ i in range n, f i • g i =
+      f (n - 1) • G n - ∑ i in range (n - 1), (f (i + 1) - f i) • G (i + 1) := by
+  by_cases hn : n = 0
+  · simp [hn]
+  · rw [range_eq_Ico, sum_Ico_by_parts f g (Nat.pos_of_ne_zero hn), sum_range_zero, smul_zero,
+      sub_zero, range_eq_Ico]
+#align finset.sum_range_by_parts Finset.sum_range_by_parts
+
+end Finset

Mathlib/Algebra/BigOperators/Order.lean

@@ -804,6 +804,9 @@ theorem IsAbsoluteValue.abv_sum [Semiring R] [OrderedSemiring S] (abv : R → S)
   (IsAbsoluteValue.toAbsoluteValue abv).sum_le _ _
 #align is_absolute_value.abv_sum IsAbsoluteValue.abv_sum
 
+--  2024-02-14
+@[deprecated] alias abv_sum_le_sum_abv := IsAbsoluteValue.abv_sum
+
 nonrec theorem AbsoluteValue.map_prod [CommSemiring R] [Nontrivial R] [LinearOrderedCommRing S]
     (abv : AbsoluteValue R S) (f : ι → R) (s : Finset ι) :
     abv (∏ i in s, f i) = ∏ i in s, abv (f i) :=

Mathlib/Algebra/Order/AbsoluteValue.lean

@@ -26,8 +26,7 @@ This file defines a bundled type of absolute values `AbsoluteValue R S`.
    value
 -/
 
-set_option autoImplicit true
-
+variable {ι α R S : Type*}
 
 /-- `AbsoluteValue R S` is the type of absolute values on `R` mapping to `S`:
 the maps that preserve `*`, are nonnegative, positive definite and satisfy the triangle equality. -/
@@ -224,8 +223,7 @@ end Ring
 end OrderedRing
 
 section OrderedCommRing
-
-variable {R S : Type*} [Ring R] [OrderedCommRing S] (abv : AbsoluteValue R S)
+variable [OrderedCommRing S] [Ring R] (abv : AbsoluteValue R S)
 
 variable [NoZeroDivisors S]
 
@@ -248,15 +246,14 @@ protected theorem le_add (a b : R) : abv a - abv b ≤ abv (a + b) := by
 lemma sub_le_add (a b : R) : abv (a - b) ≤ abv a + abv b := by
   simpa only [← sub_eq_add_neg, AbsoluteValue.map_neg] using abv.add_le a (-b)
 
-end OrderedCommRing
-
-instance {R S : Type*} [Ring R] [OrderedCommRing S] [Nontrivial R] [IsDomain S] :
-    MulRingNormClass (AbsoluteValue R S) R S :=
+instance [Nontrivial R] [IsDomain S] : MulRingNormClass (AbsoluteValue R S) R S :=
   { AbsoluteValue.subadditiveHomClass,
     AbsoluteValue.monoidWithZeroHomClass with
     map_neg_eq_map := fun f => f.map_neg
     eq_zero_of_map_eq_zero := fun f _ => f.eq_zero.1 }
 
+end OrderedCommRing
+
 section LinearOrderedRing
 
 variable {R S : Type*} [Semiring R] [LinearOrderedRing S] (abv : AbsoluteValue R S)
@@ -322,7 +319,7 @@ lemma abv_nonneg (x) : 0 ≤ abv x := abv_nonneg' x
 
 open Lean Meta Mathlib Meta Positivity Qq in
 /-- The `positivity` extension which identifies expressions of the form `abv a`. -/
-@[positivity (_ : α)]
+@[positivity _]
 def Mathlib.Meta.Positivity.evalAbv : PositivityExt where eval {_ _α} _zα _pα e := do
   let (.app f a) ← whnfR e | throwError "not abv ·"
   let pa' ← mkAppM ``abv_nonneg #[f, a]
@@ -420,14 +417,7 @@ end Ring
 end OrderedRing
 
 section OrderedCommRing
-
-variable {S : Type*} [OrderedCommRing S]
-
-section Ring
-
-variable {R : Type*} [Ring R] (abv : R → S) [IsAbsoluteValue abv]
-
-variable [NoZeroDivisors S]
+variable [OrderedCommRing S] [NoZeroDivisors S] [Ring R] (abv : R → S) [IsAbsoluteValue abv]
 
 theorem abv_neg (a : R) : abv (-a) = abv a :=
   (toAbsoluteValue abv).map_neg a
@@ -437,8 +427,6 @@ theorem abv_sub (a b : R) : abv (a - b) = abv (b - a) :=
   (toAbsoluteValue abv).map_sub a b
 #align is_absolute_value.abv_sub IsAbsoluteValue.abv_sub
 
-end Ring
-
 end OrderedCommRing
 
 section LinearOrderedCommRing