Dedekind eta e2

Mathlib/Analysis/Complex/Exponential.lean

@@ -150,6 +150,10 @@ lemma exp_nsmul' (x a p : ℂ) (n : ℕ) : exp (a * n * x / p) = exp (a * x / p)
   rw [← Complex.exp_nsmul]
   ring_nf
 
+lemma exp_nsmul' (x a p : ℂ) (n : ℕ) : exp (a * n * x / p) = exp (a * x / p) ^ n := by
+  rw [← Complex.exp_nsmul]
+  ring_nf
+
 theorem exp_nat_mul (x : ℂ) : ∀ n : ℕ, exp (n * x) = exp x ^ n
   | 0 => by rw [Nat.cast_zero, zero_mul, exp_zero, pow_zero]
   | Nat.succ n => by rw [pow_succ, Nat.cast_add_one, add_mul, exp_add, ← exp_nat_mul _ n, one_mul]

Mathlib/Analysis/SpecialFunctions/Log/Summable.lean

@@ -46,6 +46,14 @@ lemma summable_log_one_add_of_summable {f : ι → ℂ} (hf : Summable f) :
   filter_upwards [hf.norm.tendsto_cofinite_zero.eventually_le_const one_half_pos] with i hi
     using norm_log_one_add_half_le_self hi
 
+lemma tprod_one_add_ne_zero_of_summable {α : Type*} (x : α) {f : ι → α → ℂ}
+    (hf : ∀ i x, 1 + f i x ≠ 0) (hu : ∀ x : α, Summable fun n => f n x) :
+    (∏' i : ι, (1 + f i) x) ≠ 0 := by
+  simp only [Pi.add_apply, Pi.one_apply, ne_eq]
+  rw [← Complex.cexp_tsum_eq_tprod (f := fun n => 1 + f n x) (fun n => hf n x)]
+  · simp only [exp_ne_zero, not_false_eq_true]
+  · exact Complex.summable_log_one_add_of_summable (hu x)
+
 protected lemma multipliable_one_add_of_summable (hf : Summable f) :
     Multipliable (fun i ↦ 1 + f i) :=
   multipliable_of_summable_log (summable_log_one_add_of_summable hf)

Mathlib/NumberTheory/ModularForms/DedekindEta.lean

@@ -28,8 +28,6 @@ differentiable on the upper half-plane.
 open TopologicalSpace Set MeasureTheory intervalIntegral
  Metric Filter Function Complex
 
-open UpperHalfPlane hiding I
-
 open scoped Interval Real NNReal ENNReal Topology BigOperators Nat
 
 local notation "𝕢" => Periodic.qParam
@@ -80,13 +78,15 @@ lemma multipliableLocallyUniformlyOn_eta :
   · rw [hasProdUniformlyOn_iff_tendstoUniformlyOn]
     simpa [not_nonempty_iff_eq_empty.mp hN] using tendstoUniformlyOn_empty
 
-/-- Eta is non-vanishing on the upper half plane. -/
-lemma eta_ne_zero {z : ℂ} (hz : z ∈ ℍₒ) : η z ≠ 0 := by
-  apply mul_ne_zero (Periodic.qParam_ne_zero z)
+lemma eta_tprod_ne_zero {z : ℂ} (hz : z ∈ ℍₒ) : (∏' n, (1 - eta_q n z)) ≠ 0 := by
   refine tprod_one_add_ne_zero_of_summable (f := fun n ↦ -eta_q n z) ?_ ?_
   · exact fun i ↦ by simpa using one_sub_eta_q_ne_zero i hz
   · simpa [eta_q, ← summable_norm_iff] using summable_eta_q ⟨z, hz⟩
 
+/-- Eta is non-vanishing on the upper half plane. -/
+lemma eta_ne_zero {z : ℂ} (hz : z ∈ ℍₒ) : η z ≠ 0 := by
+  apply mul_ne_zero (Periodic.qParam_ne_zero z) (eta_tprod_ne_zero hz)
+
 lemma logDeriv_one_sub_cexp (r : ℂ) : logDeriv (fun z ↦ 1 - r * cexp z) =
     fun z ↦ -r * cexp z / (1 - r * cexp z) := by
   ext z
@@ -116,12 +116,56 @@ lemma tsum_logDeriv_eta_q (z : ℂ) : ∑' n, logDeriv (fun x ↦ 1 - eta_q n x)
   rw [tsum_congr (one_sub_eta_logDeriv_eq z), ← tsum_mul_left]
   grind
 
-theorem differentiableAt_eta_of_mem_upperHalfPlaneSet {z : ℂ} (hz : z ∈ ℍₒ) :
-    DifferentiableAt ℂ eta z := by
-  apply DifferentiableAt.mul (by fun_prop)
-  refine (multipliableLocallyUniformlyOn_eta.hasProdLocallyUniformlyOn.differentiableOn ?_
+lemma differentiableAt_eta_tprod {z : ℂ} (hz : z ∈ ℍₒ) :
+    DifferentiableAt ℂ (fun x ↦ ∏' n, (1 - eta_q n x)) z := by
+  apply (multipliableLocallyUniformlyOn_eta.hasProdLocallyUniformlyOn.differentiableOn ?_
     isOpen_upperHalfPlaneSet z hz).differentiableAt (isOpen_upperHalfPlaneSet.mem_nhds hz)
   filter_upwards with b
   simpa [Finset.prod_fn] using DifferentiableOn.finset_prod (by fun_prop)
 
+theorem differentiableAt_eta_of_mem_upperHalfPlaneSet {z : ℂ} (hz : z ∈ ℍₒ) :
+    DifferentiableAt ℂ eta z := by
+  apply DifferentiableAt.mul (by fun_prop) (differentiableAt_eta_tprod hz)
+
+lemma summable_log_deriv_one_sub_eta_q {z : ℂ} (hz : z ∈ ℍₒ) :
+    Summable fun i ↦ logDeriv (fun x ↦ 1 - eta_q i x) z := by
+  simp only [one_sub_eta_logDeriv_eq]
+  apply ((summable_nat_add_iff 1).mpr ((summable_norm_pow_mul_geometric_div_one_sub (r := 𝕢 1 z) 1
+    (by simpa [Periodic.qParam] using UpperHalfPlane.norm_exp_two_pi_I_lt_one ⟨z, hz⟩)).mul_left
+    (-2 * π * I))).congr
+  intro b
+  field_simp [one_sub_eta_q_ne_zero b hz]
+  ring
+
+lemma logDeriv_q_term (z : ℍ) : logDeriv (𝕢 24) ↑z  =  2 * ↑π * I / 24 := by
+  have : (𝕢 24) = (fun z ↦ cexp (z)) ∘ (fun z => (2 * ↑π * I / 24) * z)  := by
+    ext y
+    simp only [Periodic.qParam, ofReal_ofNat, comp_apply]
+    ring_nf
+  rw [this, logDeriv_comp (by fun_prop) (by fun_prop), deriv_const_mul _ (by fun_prop)]
+  simp only [LogDeriv_exp, Pi.one_apply, deriv_id'', mul_one, one_mul]
+
+lemma eta_logDeriv (z : ℍ) : logDeriv ModularForm.eta z = (π * I / 12) * E2 z := by
+  unfold ModularForm.eta
+  rw [logDeriv_mul (UpperHalfPlane.coe z) (by simp [ne_eq, exp_ne_zero, not_false_eq_true,
+    Periodic.qParam]) (eta_tprod_ne_zero z.2) (by fun_prop) (differentiableAt_eta_tprod z.2)]
+  have HG := logDeriv_tprod_eq_tsum isOpen_upperHalfPlaneSet (x := z)
+    (f := fun n x => 1 - eta_q n x) (fun i ↦ one_sub_eta_q_ne_zero i z.2)
+    (by simp_rw [eta_q_eq_pow]; fun_prop) (summable_log_deriv_one_sub_eta_q z.2)
+    (multipliableLocallyUniformlyOn_eta ) (eta_tprod_ne_zero z.2)
+  rw [show z.1 = UpperHalfPlane.coe z by rfl] at HG
+  simp only [logDeriv_q_term z, HG, tsum_logDeriv_eta_q z, E2, one_div,
+    mul_inv_rev, Pi.smul_apply, smul_eq_mul]
+  rw [G2_q_exp, riemannZeta_two, ← tsum_pow_div_one_sub_eq_tsum_sigma
+    (by apply UpperHalfPlane.norm_exp_two_pi_I_lt_one z), mul_sub, sub_eq_add_neg, mul_add]
+  congr 1
+  · field_simp
+    ring
+  · field_simp [tsum_pnat_eq_tsum_succ (f := fun n ↦ n * cexp (2 * π * I * z) ^ n
+      / (1 - cexp (2 * π * I * z) ^ n )), eta_q_eq_pow]
+    simp_rw [← tsum_mul_left, ← tsum_mul_right, ← tsum_neg]
+    congr
+    ext n
+    ring_nf
+
 end ModularForm

Mathlib/NumberTheory/ModularForms/EisensteinSeries/Defs.lean

@@ -140,6 +140,68 @@ def gammaSetDivGcdSigmaEquiv : (Fin 2 → ℤ) ≃ (Σ r : ℕ, gammaSet 1 r 0)
 lemma gammaSetDivGcdSigmaEquiv_symm_eq (v : Σ r : ℕ, gammaSet 1 r 0) :
     (gammaSetDivGcdSigmaEquiv.symm v) = v.2 := rfl
 
+/-- The map from `Fin 2 → ℤ` sending `![a,b]` to `a.gcd b`. -/
+def fin_to_gcd_map (v : Fin 2 → ℤ) : ℕ := (v 0).gcd (v 1)
+
+/-- The set of pairs of integers whose gcd is `N`, defined as the fiber of
+`fin_to_gcd_map` at `N`. -/
+def gammaSetN (N : ℕ) : Set (Fin 2 → ℤ) := fin_to_gcd_map ⁻¹' {N}
+
+/-- An abbreviation of the map which divides a integer vector by an integer. -/
+abbrev div_N_map (N : ℤ) {m : ℕ} (v : Fin m → ℤ) : Fin m → ℤ := fun i => v i / N
+
+lemma gammaSet_top_mem (v : Fin 2 → ℤ) : v ∈ gammaSet 1 0 ↔ IsCoprime (v 0) (v 1) := by
+  simpa [gammaSet] using fun h ↦ Subsingleton.eq_zero (Int.cast ∘ v)
+
+lemma gammaSetN_div_N {N : ℕ} {v : Fin 2 → ℤ} (hv : v ∈ gammaSetN N) (i : Fin 2) :
+   (N : ℤ) ∣ v i  := by
+  simp only [gammaSetN, mem_preimage, fin_to_gcd_map, Fin.isValue, mem_singleton_iff] at *
+  fin_cases i <;> simp [← hv, Int.gcd_dvd_left, Int.gcd_dvd_right]
+
+lemma gammaSetN_to_gammaSet10_bijection {N : ℕ} (hN : N ≠ 0) :
+    Set.BijOn (div_N_map N) (gammaSetN N) (gammaSet 1 0) := by
+  refine ⟨?_, ?_, ?_⟩
+  · intro x hx
+    simp only [ne_eq, gammaSetN, mem_preimage, fin_to_gcd_map, Fin.isValue, mem_singleton_iff,
+      gammaSet_top_mem] at *
+    rw [← hx] at hN ⊢
+    apply isCoprime_div_gcd_div_gcd' (by simpa using hN)
+  · intro x hx v hv hv2
+    ext i
+    · apply (Int.ediv_left_inj (gammaSetN_div_N hx i) (gammaSetN_div_N hv i)).mp (congr_fun hv2 i)
+  · intro x hx
+    use N • x
+    simp only [gammaSetN, nsmul_eq_mul, mem_preimage, fin_to_gcd_map, Fin.isValue, Pi.mul_apply,
+      Pi.natCast_apply, mem_singleton_iff]
+    constructor
+    · rw [gammaSet_top_mem, Int.isCoprime_iff_gcd_eq_one] at hx
+      simp [Int.gcd_mul_left, hx]
+    · ext i
+      simp_all [div_N_map]
+
+lemma gammaSetN_map_eq {N : ℕ} (v : gammaSetN N) : v.1 = N • (div_N_map N v) := by
+  by_cases hN : N = 0
+  · have hv := v.2
+    simp only [hN, gammaSetN, mem_preimage, fin_to_gcd_map, Fin.isValue, mem_singleton_iff,
+      Int.gcd_eq_zero_iff, CharP.cast_eq_zero, zero_nsmul] at *
+    ext i
+    fin_cases i <;> simp [hv]
+  · ext i
+    simp_all [Pi.smul_apply, div_N_map, ← Int.mul_ediv_assoc _ (gammaSetN_div_N v.2 i)]
+
+/-- The equivalence between `gammaSetN` and `gammaSet` for non-zero `N`. -/
+def gammaSetN_Equiv {N : ℕ} (hN : N ≠ 0) : gammaSetN N ≃ gammaSet 1 0 := by
+  apply Set.BijOn.equiv _ (gammaSetN_to_gammaSet10_bijection hN)
+
+/-- The equivalence between `(Fin 2 → ℤ)` and `Σ  n : ℕ, gammaSetN n)` . -/
+def GammaSet_top_Equiv : (Fin 2 → ℤ) ≃ (Σ  n : ℕ, gammaSetN n) :=
+  (Equiv.sigmaFiberEquiv fin_to_gcd_map).symm
+
+@[simp]
+lemma GammaSet_top_Equiv_symm_eq (v : Σ n : ℕ, gammaSetN n) :
+    (GammaSet_top_Equiv.symm v) = v.2 := by
+  simp [GammaSet_top_Equiv, fin_to_gcd_map, Equiv.sigmaFiberEquiv]
+
 end gammaSet_def
 
 variable {N a r} [NeZero r]

Mathlib/NumberTheory/ModularForms/EisensteinSeries/E2.lean

@@ -0,0 +1,173 @@
+/-
+Copyright (c) 2025 Chris Birkbeck. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Chris Birkbeck
+-/
+import Mathlib.Algebra.Order.Ring.Star
+import Mathlib.Analysis.CStarAlgebra.Classes
+import Mathlib.Data.Int.Star
+import Mathlib.NumberTheory.LSeries.RiemannZeta
+import Mathlib.NumberTheory.ModularForms.EisensteinSeries.UniformConvergence
+import Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
+
+/-!
+# Eisenstein Series E2
+
+We define the Eisenstein series `E2` of weight `2` and level `1` as a limit of partial sums
+over non-symmetric intervals.
+
+-/
+
+open ModularForm EisensteinSeries TopologicalSpace  intervalIntegral
+  Metric Filter Function Complex MatrixGroups Finset ArithmeticFunction
+
+open _root_.UpperHalfPlane hiding I
+
+open scoped Interval Real Topology BigOperators Nat
+
+noncomputable section
+
+
+/-- This is an auxilary summand used to define the Eisenstein serires `G2`. -/
+def e2Summand (m : ℤ) (z : ℍ) : ℂ := ∑' (n : ℤ), eisSummand 2 ![m, n] z
+
+lemma e2Summand_summable (m : ℤ) (z : ℍ) : Summable (fun n => eisSummand 2 ![m, n] z) := by
+  apply (linear_right_summable z m (k := 2) (by omega)).congr
+  simp [eisSummand]
+
+@[simp]
+lemma e2Summand_zero_eq_riemannZeta_two (z : ℍ) : e2Summand 0 z = 2 * riemannZeta 2 := by
+  simpa [e2Summand, eisSummand] using
+    (two_riemannZeta_eq_tsum_int_inv_even_pow (k := 2) (by omega) (by simp)).symm
+
+/-- The Eisenstein series of weight `2` and level `1` defined as the limit as `N` tends to
+infinity of the partial sum of `m` in `[N,N)` of `e2Summand m`. This sum over symmetric
+intervals is handy in showing it is Cauchy. -/
+def G2 : ℍ → ℂ := fun z => limUnder atTop (fun N : ℕ => ∑ m ∈ Icc (-N : ℤ) N, e2Summand m z)
+
+/-- The normalised Eisenstein series of weight `2` and level `1`. -/
+def E2 : ℍ → ℂ := (1 / (2 * riemannZeta 2)) •  G2
+
+/-- This function measures the defect in `E2` being a modular form. -/
+def D2 (γ : SL(2, ℤ)) : ℍ → ℂ := fun z => (2 * π * I * γ 1 0) / (denom γ z)
+
+--moves these two elsewhere
+lemma Icc_succ_succ (n : ℕ) : Finset.Icc (-(n + 1) : ℤ) (n + 1) = Finset.Icc (-n : ℤ) n ∪
+  {(-(n + 1) : ℤ), (n + 1 : ℤ)} := by
+  refine Finset.ext_iff.mpr ?_
+  intro a
+  simp only [neg_add_rev, Int.reduceNeg, Finset.mem_Icc, add_neg_le_iff_le_add, Finset.union_insert,
+    Finset.mem_insert, Finset.mem_union, Finset.mem_singleton]
+  omega
+
+lemma sum_Icc_of_even_eq_range {α : Type*} [CommRing α] (f : ℤ → α) (hf : ∀ n, f n = f (-n))
+    (N : ℕ) : ∑ m ∈  Finset.Icc (-N : ℤ) N, f m =  2 * ∑ m ∈ Finset.range (N + 1), f m  - f 0 := by
+  induction' N with N ih
+  · simp [two_mul]
+  · have := Icc_succ_succ N
+    simp only [neg_add_rev, Int.reduceNeg,  Nat.cast_add, Nat.cast_one] at *
+    rw [this, Finset.sum_union (by simp), Finset.sum_pair (by omega), ih]
+    nth_rw 2 [Finset.sum_range_succ]
+    have HF := hf (N + 1)
+    simp only [neg_add_rev, Int.reduceNeg] at HF
+    rw [← HF]
+    ring_nf
+    norm_cast
+
+lemma G2_partial_sum_eq (z : ℍ) (N : ℕ) : (∑ m ∈ Icc (-N : ℤ) N, e2Summand m z) =
+    (2 * riemannZeta 2) + (∑ m ∈ Finset.range N, 2 * (-2 * ↑π * I) ^ 2  *
+    ∑' n : ℕ+, n  * cexp (2 * ↑π * I * (m + 1) * z) ^ (n : ℕ)) := by
+  rw [sum_Icc_of_even_eq_range, Finset.sum_range_succ', mul_add]
+  · nth_rw 2 [two_mul]
+    ring_nf
+    have (a : ℕ):= EisensteinSeries.qExpansion_identity_pnat (k := 1) (by omega) ⟨(a + 1) * z, by
+      have ha : 0 < a + (1 : ℝ) := by linarith
+      simpa [ha] using z.2⟩
+    simp only [coe_mk_subtype, add_comm, Nat.reduceAdd, one_div, mul_comm, mul_neg, even_two,
+      Even.neg_pow, Nat.factorial_one, Nat.cast_one, div_one, pow_one, e2Summand, eisSummand,
+      Nat.cast_add, Fin.isValue, Matrix.cons_val_zero, Int.cast_add, Int.cast_natCast, Int.cast_one,
+      Matrix.cons_val_one, Matrix.cons_val_fin_one, Int.reduceNeg, zpow_neg, mul_sum, Int.cast_zero,
+      zero_mul, add_zero, I_sq, neg_mul, one_mul] at *
+    congr
+    · simpa using (two_riemannZeta_eq_tsum_int_inv_even_pow (k := 2) (by omega) (by simp)).symm
+    · ext a
+      norm_cast at *
+      simp_rw [this a, ← tsum_mul_left, ← tsum_neg,ofReal_mul, ofReal_ofNat, mul_pow, I_sq, neg_mul,
+        one_mul, Nat.cast_add, Nat.cast_one, mul_neg, ofReal_pow]
+      apply tsum_congr
+      intro b
+      ring_nf
+  · intro n
+    simp only [e2Summand, eisSummand, Fin.isValue, Matrix.cons_val_zero, Matrix.cons_val_one,
+      Matrix.cons_val_fin_one, Int.reduceNeg, zpow_neg, Int.cast_neg, neg_mul]
+    nth_rw 2 [← tsum_int_eq_tsum_neg]
+    apply tsum_congr
+    intro b
+    norm_cast
+    ring_nf
+    aesop
+
+private lemma aux_tsum_identity (z : ℍ) : ∑' m : ℕ, (2 * (-2 * ↑π * I) ^ 2  *
+    ∑' n : ℕ+, n * cexp (2 * ↑π * I * (m + 1) * z) ^ (n : ℕ))  =
+    -8 * π ^ 2 * ∑' (n : ℕ+), (sigma 1 n) * cexp (2 * π * I * z) ^ (n : ℕ) := by
+  have := tsum_prod_pow_cexp_eq_tsum_sigma 1 z
+  rw [tsum_pnat_eq_tsum_succ (fun d =>
+    ∑' (c : ℕ+), (c ^ 1 : ℂ) * cexp (2 * ↑π * I * d * z) ^ (c : ℕ))] at this
+  simp only [neg_mul, even_two, Even.neg_pow, ← tsum_mul_left, ← this, Nat.cast_add, Nat.cast_one]
+  apply tsum_congr2
+  intro b c
+  rw [mul_pow, I_sq, mul_neg, mul_one]
+  ring
+
+theorem G2_tendsto (z : ℍ) : Tendsto (fun N ↦ ∑ x ∈ range N, 2 * (2 * ↑π * I) ^ 2 *
+    ∑' (n : ℕ+), n * cexp (2 * ↑π * I * (↑x + 1) * ↑z) ^ (n : ℕ)) atTop
+    (𝓝 (-8 * ↑π ^ 2 * ∑' (n : ℕ+), ↑((σ 1) ↑n) * cexp (2 * ↑π * I * ↑z) ^ (n : ℕ))) := by
+  rw [← aux_tsum_identity]
+  have hf : Summable fun m : ℕ => ( 2 * (-2 * ↑π * I) ^ 2 *
+      ∑' n : ℕ+, n ^ ((2 - 1)) * Complex.exp (2 * ↑π * I * (m + 1) * z) ^ (n : ℕ)) := by
+    apply Summable.mul_left
+    have := (summable_prod_aux 1 z).prod_symm.prod
+    have h0 := pnat_summable_iff_summable_succ
+      (f := fun b ↦ ∑' (c : ℕ+), c * cexp (2 * ↑π * I * ↑↑b * ↑z) ^ (c : ℕ))
+    simp at *
+    rw [← h0]
+    apply this
+  simpa using (hf.hasSum).comp tendsto_finset_range
+
+lemma G2_cauchy (z : ℍ) : CauchySeq (fun N : ℕ => ∑ m ∈ Icc (-N : ℤ) N, e2Summand m z) := by
+  conv =>
+    enter [1]
+    ext n
+    rw [G2_partial_sum_eq]
+  apply CauchySeq.const_add
+  apply Filter.Tendsto.cauchySeq (x := -8 * π ^ 2 *
+    ∑' (n : ℕ+), (σ 1 n) * cexp (2 * π * I * z) ^ (n : ℕ))
+  simpa using G2_tendsto z
+
+lemma G2_q_exp (z : ℍ) : G2 z = (2 * riemannZeta 2) - 8 * π ^ 2 *
+  ∑' n : ℕ+, sigma 1 n * cexp (2 * π * I * z) ^ (n : ℕ) := by
+  rw [G2, Filter.Tendsto.limUnder_eq, sub_eq_add_neg]
+  conv =>
+    enter [1]
+    ext N
+    rw [G2_partial_sum_eq z N]
+  exact Filter.Tendsto.add (by simp) (by simpa using G2_tendsto z)
+
+
+
+/- lemma Asymptotics.IsBigO.map {α β ι γ : Type*} [Norm α] [Norm β] {f : ι → α} {g : ι → β}
+  {p : Filter ι} (hf : f =O[p] g) (c : γ → ι) :
+    (fun (n : γ) => f (c n)) =O[p.comap c] fun n => g (c n) := by
+  rw [isBigO_iff] at *
+  obtain ⟨C, hC⟩ := hf
+  refine ⟨C, ?_⟩
+  simp only [eventually_comap] at *
+  filter_upwards [hC] with n hn
+  exact fun a ha ↦ Eq.mpr (id (congrArg (fun _a ↦ ‖f _a‖ ≤ C * ‖g _a‖) ha)) hn
+
+lemma Asymptotics.IsBigO.nat_of_int {α β : Type*} [Norm α] [SeminormedAddCommGroup β] {f : ℤ → α}
+    {g : ℤ → β} (hf : f =O[cofinite] g) : (fun (n : ℕ) => f n) =O[cofinite] fun n => g n := by
+  have := Asymptotics.IsBigO.map hf Nat.cast
+  simp only [Int.cofinite_eq, isBigO_sup, comap_sup, Asymptotics.isBigO_sup] at *
+  rw [Nat.cofinite_eq_atTop]
+  simpa using this.2 -/

Mathlib/NumberTheory/ModularForms/EisensteinSeries/Summable.lean

@@ -61,6 +61,22 @@ lemma abs_norm_eq_max_natAbs_neg (n : ℕ) : ‖![1, -(n + 1 : ℤ)]‖ = n + 1
     Matrix.cons_val_fin_one]
   norm_cast
 
+lemma abs_norm_eq_max_natAbs (n : ℕ) :
+    ‖![1, (n + 1 : ℤ)]‖ = n + 1 := by
+  simp only [Nat.succ_eq_add_one, Nat.reduceAdd, EisensteinSeries.norm_eq_max_natAbs, Fin.isValue,
+    Matrix.cons_val_zero, isUnit_one, Int.natAbs_of_isUnit, Matrix.cons_val_one,
+    Matrix.cons_val_fin_one, Nat.cast_max, Nat.cast_one]
+  norm_cast
+  simp
+
+lemma abs_norm_eq_max_natAbs_neg (n : ℕ) :
+    ‖![1, -(n + 1 : ℤ)]‖ = n + 1 := by
+  simp only [EisensteinSeries.norm_eq_max_natAbs, Fin.isValue, Matrix.cons_val_zero, isUnit_one,
+    Int.natAbs_of_isUnit, Matrix.cons_val_one, Matrix.cons_val_fin_one, Nat.cast_max,
+    Int.natAbs_neg]
+  norm_cast
+  simp
+
 section bounding_functions
 
 /-- Auxiliary function used for bounding Eisenstein series, defined as

Mathlib/Topology/Algebra/InfiniteSum/NatInt.lean

@@ -527,10 +527,17 @@ theorem Summable.alternating {α} [Ring α]
 
 end IsUniformGroup
 
+theorem tsum_int_eq_tsum_neg {α : Type*} [AddCommMonoid α] [TopologicalSpace α] (f : ℤ → α) :
+    ∑' d, f (-d) = ∑' d, f d := by
+  rw [show (fun d => f (-d)) = (fun d => f d) ∘ (Equiv.neg ℤ) by ext; simp]
+  apply (Equiv.neg ℤ).tsum_eq
+
 end Int
 
 section PNat
 
+variable {R : Type*} {α : Type*} [AddMonoidWithOne R] [TopologicalSpace α] [CommMonoid α]
+
 @[to_additive]
 theorem multipliable_pnat_iff_multipliable_succ {f : ℕ → M} :
     Multipliable (fun x : ℕ+ ↦ f x) ↔ Multipliable fun x ↦ f (x + 1) :=