From 66e51de29213c7c63525909f746be19c4767b2f9 Mon Sep 17 00:00:00 2001
From: jtristan <trjohnb@amazon.com>
Date: Tue, 4 Jun 2024 13:24:45 -0400
Subject: [PATCH 1/2] More abstract tsum shift

---
 SampCert/Util/Shift.lean | 17 ++++++++++-------
 1 file changed, 10 insertions(+), 7 deletions(-)

diff --git a/SampCert/Util/Shift.lean b/SampCert/Util/Shift.lean
index 57c2aa2c..5a682e04 100644
--- a/SampCert/Util/Shift.lean
+++ b/SampCert/Util/Shift.lean
@@ -3,8 +3,9 @@ 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
@@ -12,12 +13,14 @@ import Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
 This file contains lemmas about invariance of sums under integer shifts.
 -/
 
+variable {M : Type*} [AddCommGroup M] [UniformSpace M] [T2Space M] [UniformAddGroup M] [CompleteSpace M] {m m' : M}
+
 open Summable
 
 /--
 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 +39,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 +73,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
@@ -116,19 +119,19 @@ theorem tsum_shift₂ (f : ℤ → ℝ) (μ : ℕ)
 /--
 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

From c6d5c46bf2db8f1c35eabc86c83998f2ee840b7c Mon Sep 17 00:00:00 2001
From: jtristan <trjohnb@amazon.com>
Date: Tue, 4 Jun 2024 15:39:15 -0400
Subject: [PATCH 2/2] refining type classes constraints

---
 SampCert/Util/Shift.lean | 14 +++++++++++++-
 1 file changed, 13 insertions(+), 1 deletion(-)

diff --git a/SampCert/Util/Shift.lean b/SampCert/Util/Shift.lean
index 5a682e04..36698039 100644
--- a/SampCert/Util/Shift.lean
+++ b/SampCert/Util/Shift.lean
@@ -13,10 +13,14 @@ import Mathlib.Topology.Algebra.InfiniteSum.NatInt
 This file contains lemmas about invariance of sums under integer shifts.
 -/
 
-variable {M : Type*} [AddCommGroup M] [UniformSpace M] [T2Space M] [UniformAddGroup M] [CompleteSpace M] {m m' : M}
+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.
 -/
@@ -116,6 +120,12 @@ theorem tsum_shift₂ (f : ℤ → M) (μ : ℕ)
   . 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.
 -/
@@ -157,3 +167,5 @@ theorem tsum_shift (f : ℤ → M) (μ : ℤ)
     apply tsum_congr
     intro b
     congr
+
+end B