Shift abstraction

SampCert/Util/Shift.lean

@@ -3,21 +3,28 @@ Copyright (c) 2024 Amazon.com, Inc. or its affiliates. All Rights Reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Jean-Baptiste Tristan
 -/
+import Mathlib.Topology.Algebra.InfiniteSum.Defs
 import Mathlib.Topology.Algebra.InfiniteSum.Basic
-import Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
+import Mathlib.Topology.Algebra.InfiniteSum.NatInt
 
 /-!
 # Shift Util
 
 This file contains lemmas about invariance of sums under integer shifts.
 -/
 
+variable {M : Type*} {m m' : M}
+
 open Summable
 
+section A
+
+variable [AddCommGroup M] [UniformSpace M] [T2Space M] [UniformAddGroup M]
+
 /--
 A series is right-ℕ-shift-invariant provided its shifted positive and negative parts are summable.
 -/
-theorem tsum_shift₁ (f : ℤ → ℝ) (μ : ℕ)
+theorem tsum_shift₁ (f : ℤ → M) (μ : ℕ)
   (h2 : ∀ μ : ℕ, Summable fun x : ℕ => f (x + μ))
   (h3 : ∀ μ : ℕ, Summable fun x : ℕ => f (-(x + 1) + μ))
   :
@@ -36,7 +43,7 @@ theorem tsum_shift₁ (f : ℤ → ℝ) (μ : ℕ)
       rw [add_comm]
     conv =>
       right
-      rw [@tsum_of_nat_of_neg_add_one ℝ _ _ _ _ (fun x : ℤ => f (x + μ)) (h2 μ) (h3 μ)]
+      rw [@tsum_of_nat_of_neg_add_one M _ _ _ _ (fun x : ℤ => f (x + μ)) (h2 μ) (h3 μ)]
     congr 1
     conv =>
       right
@@ -70,7 +77,7 @@ theorem tsum_shift₁ (f : ℤ → ℝ) (μ : ℕ)
 /--
 A series is left-ℕ-shift-invariant provided its shifted positive and negative parts are summable.
 -/
-theorem tsum_shift₂ (f : ℤ → ℝ) (μ : ℕ)
+theorem tsum_shift₂ (f : ℤ → M) (μ : ℕ)
   (h2 : ∀ μ : ℕ, Summable fun x : ℕ => f (x - μ))
   (h3 : ∀ μ : ℕ, Summable fun x : ℕ => f (-(x + 1) - μ)) :
   ∑' x : ℤ, f (x - μ) = (∑' x : ℤ, f x) := by
@@ -113,22 +120,28 @@ theorem tsum_shift₂ (f : ℤ → ℝ) (μ : ℕ)
   . exact (h2 μ)
   . exact (h3 μ)
 
+end A
+
+section B
+
+variable [AddCommGroup M] [UniformSpace M] [T2Space M] [UniformAddGroup M] [CompleteSpace M]
+
 /--
 A series is invariant under integer shifts provided its shifted positive and negative parts are summable.
 -/
-theorem tsum_shift (f : ℤ → ℝ) (μ : ℤ)
+theorem tsum_shift (f : ℤ → M) (μ : ℤ)
   (h₀ : ∀ μ : ℤ, Summable fun x : ℤ => f (x + μ)) :
   ∑' x : ℤ, f (x + μ) = (∑' x : ℤ, f x) := by
   have h : ∀ μ : ℤ, Summable fun x : ℕ => f (x + μ) := by
     intro μ
-    have A := @summable_int_iff_summable_nat_and_neg_add_zero ℝ _ _ _ _ (fun x => f (x + μ))
+    have A := @summable_int_iff_summable_nat_and_neg_add_zero M _ _ _ _ (fun x => f (x + μ))
     replace A := A.1 (h₀ μ)
     cases A
     rename_i X Y
     exact X
   have h' : ∀ μ : ℤ, Summable fun x : ℕ => f (-(x + 1) + μ) := by
     intro μ
-    have A := @summable_int_iff_summable_nat_and_neg_add_zero ℝ _ _ _ _ (fun x => f (x + μ))
+    have A := @summable_int_iff_summable_nat_and_neg_add_zero M _ _ _ _ (fun x => f (x + μ))
     replace A := A.1 (h₀ μ)
     cases A
     rename_i X Y
@@ -154,3 +167,5 @@ theorem tsum_shift (f : ℤ → ℝ) (μ : ℤ)
     apply tsum_congr
     intro b
     congr
+
+end B