feat(NumberTheory/ModularForms/EisensteinSeries/Summable): add auxiliary E2 lemmas (leanprover-community#32955)

This contains a series of lemmas that are needed in leanprover-community#32585 to prove how E2 transforms under the slash action.

Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>

Author: CBirkbeck

Mathlib.lean

@@ -5356,6 +5356,7 @@ public import Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber
 public import Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
 public import Mathlib.NumberTheory.Transcendental.Liouville.Measure
 public import Mathlib.NumberTheory.Transcendental.Liouville.Residual
+public import Mathlib.NumberTheory.TsumDivisorsAntidiagonal
 public import Mathlib.NumberTheory.TsumDivsorsAntidiagonal
 public import Mathlib.NumberTheory.VonMangoldt
 public import Mathlib.NumberTheory.WellApproximable

Mathlib/Analysis/Complex/IntegerCompl.lean

@@ -58,4 +58,10 @@ lemma upperHalfPlane_inter_integerComplement :
   simp only [Set.mem_inter_iff, Set.mem_setOf_eq, and_iff_left_iff_imp]
   exact fun hz ↦ UpperHalfPlane.coe_mem_integerComplement ⟨z, hz⟩
 
+lemma UpperHalfPlane.int_div_mem_integerComplement (z : ℍ) {n : ℤ} (hn : n ≠ 0) :
+    n / (z : ℂ) ∈ ℂ_ℤ := by
+  rintro ⟨_, hm⟩
+  have : (n / (z : ℂ)).im ≠ 0:= by simp [div_im, hn, z.im_pos.ne', ne_zero z]
+  simpa [← hm]
+
 end Complex

Mathlib/Analysis/Complex/UpperHalfPlane/Basic.lean

@@ -157,6 +157,10 @@ theorem normSq_ne_zero (z : ℍ) : Complex.normSq (z : ℂ) ≠ 0 :=
 theorem im_inv_neg_coe_pos (z : ℍ) : 0 < (-z : ℂ)⁻¹.im := by
   simpa [neg_div] using div_pos z.property (normSq_pos z)
 
+lemma im_pnat_div_pos (n : ℕ) [NeZero n] (z : ℍ) : 0 < (-(n : ℂ) / z).im := by
+  suffices 0 < n * z.im / Complex.normSq z by simpa [Complex.div_im, neg_div]
+  positivity [NeZero.ne n, z.normSq_pos]
+
 lemma ne_nat (z : ℍ) : ∀ n : ℕ, z.1 ≠ n := by
   intro n
   have h1 := z.2

Mathlib/NumberTheory/LSeries/RiemannZeta.lean

@@ -209,7 +209,8 @@ lemma two_mul_riemannZeta_eq_tsum_int_inv_pow_of_even {k : ℕ} (hk : 2 ≤ k) (
     norm_cast
     simp [h0, zeta_eq_tsum_one_div_nat_add_one_cpow (s := k) (by simp [hkk]),
       tsum_pnat_eq_tsum_succ (f := fun n => ((n : ℂ) ^ k)⁻¹)]
-  · simp [Even.neg_pow hk2]
+  · intro n
+    simp [Even.neg_pow hk2]
   · exact (Summable.of_nat_of_neg (by simp [hkk]) (by simp [hkk])).of_norm
 
 /-- The residue of `ζ(s)` at `s = 1` is equal to 1. -/

Mathlib/NumberTheory/ModularForms/EisensteinSeries/QExpansion.lean

@@ -10,7 +10,7 @@ public import Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
 public import Mathlib.NumberTheory.LSeries.Dirichlet
 public import Mathlib.NumberTheory.LSeries.HurwitzZetaValues
 public import Mathlib.NumberTheory.ModularForms.EisensteinSeries.Basic
-public import Mathlib.NumberTheory.TsumDivsorsAntidiagonal
+public import Mathlib.NumberTheory.TsumDivisorsAntidiagonal
 
 /-!
 # Eisenstein series q-expansions

Mathlib/NumberTheory/ModularForms/EisensteinSeries/Summable.lean

@@ -159,12 +159,12 @@ lemma summand_bound_of_mem_verticalStrip {k : ℝ} (hk : 0 ≤ k) (x : Fin 2 →
   exact Real.rpow_le_rpow_of_nonpos (r_pos _) (r_lower_bound_on_verticalStrip z hB hz)
     (neg_nonpos.mpr hk)
 
-lemma linear_isTheta_right (c : ℤ) (z : ℂ) :
-    (fun (d : ℤ) ↦ (c * z + d)) =Θ[cofinite] fun n ↦ (n : ℝ) := by
-  refine Asymptotics.IsLittleO.add_isTheta ?_ (Int.cast_complex_isTheta_cast_real)
-  rw [isLittleO_const_left]
-  exact Or.inr
-    (tendsto_norm_comp_cofinite_atTop_of_isClosedEmbedding Int.isClosedEmbedding_coe_real)
+lemma linear_isTheta_right_add (c e : ℤ) (z : ℂ) :
+    (fun d : ℤ ↦ c * z + d + e) =Θ[cofinite] fun n ↦ (n : ℝ) := by
+  apply IsTheta.add_isLittleO <;>
+  [refine Asymptotics.IsLittleO.add_isTheta ?_ (Int.cast_complex_isTheta_cast_real); skip] <;>
+  simpa [-Int.cofinite_eq] using
+    .inr <| tendsto_norm_comp_cofinite_atTop_of_isClosedEmbedding Int.isClosedEmbedding_coe_real
 
 lemma linear_isTheta_left (d : ℤ) {z : ℂ} (hz : z ≠ 0) :
     (fun (c : ℤ) ↦ (c * z + d)) =Θ[cofinite] fun n ↦ (n : ℝ) := by
@@ -174,14 +174,28 @@ lemma linear_isTheta_left (d : ℤ) {z : ℂ} (hz : z ≠ 0) :
   · simp only [isLittleO_const_left, Int.cast_eq_zero,
       tendsto_norm_comp_cofinite_atTop_of_isClosedEmbedding Int.isClosedEmbedding_coe_real, or_true]
 
+lemma linear_inv_isBigO_right_add (c e : ℤ) (z : ℂ) :
+    (fun (d : ℤ) ↦ (c * z + d + e)⁻¹) =O[cofinite] fun n ↦ (n : ℝ)⁻¹ :=
+  (linear_isTheta_right_add c e z).inv.isBigO
+
 lemma linear_inv_isBigO_right (c : ℤ) (z : ℂ) :
-    (fun (d : ℤ) ↦ (c * z + d)⁻¹) =O[cofinite] fun n ↦ (n : ℝ)⁻¹ :=
-  (linear_isTheta_right c z).inv.isBigO
+    (fun (d : ℤ) ↦ (c * z + d)⁻¹) =O[cofinite] fun n ↦ (n : ℝ)⁻¹ := by
+  grind [add_zero, (linear_isTheta_right_add c 0 z).inv.isBigO]
 
 lemma linear_inv_isBigO_left (d : ℤ) {z : ℂ} (hz : z ≠ 0) :
     (fun (c : ℤ) ↦ (c * z + d)⁻¹) =O[cofinite] fun n ↦ (n : ℝ)⁻¹ :=
   (linear_isTheta_left d hz).inv.isBigO
 
+lemma tendsto_zero_inv_linear (z : ℂ) (b : ℤ) :
+    Tendsto (fun d : ℕ ↦ 1 / ((b : ℂ) * z + d)) atTop (𝓝 0) := by
+  apply IsBigO.trans_tendsto ?_ tendsto_inv_atTop_nhds_zero_nat (F'' := ℝ)
+  have := (isBigO_sup.mp (Int.cofinite_eq ▸ linear_inv_isBigO_right b z)).2
+  simpa [← Nat.map_cast_int_atTop, isBigO_map]
+
+lemma tendsto_zero_inv_linear_sub (z : ℂ) (b : ℤ) :
+    Tendsto (fun d : ℕ ↦ 1 / ((b : ℂ) * z - d)) atTop (𝓝 0) := by
+  grind [neg_zero, (tendsto_zero_inv_linear z (-b)).neg]
+
 end bounding_functions
 
 /-- The function `ℤ ^ 2 → ℝ` given by `x ↦ ‖x‖ ^ (-k)` is summable if `2 < k`. We prove this by
@@ -216,9 +230,9 @@ lemma summable_inv_of_isBigO_rpow_inv {α : Type*} [NormedField α] [CompleteSpa
 lemma linear_right_summable (z : ℂ) (c : ℤ) {k : ℤ} (hk : 2 ≤ k) :
     Summable fun d : ℤ ↦ ((c * z + d) ^ k)⁻¹ := by
   apply summable_inv_of_isBigO_rpow_inv (a := k) (by norm_cast)
-  lift k to ℕ using (by lia)
-  simp only [zpow_natCast, Int.cast_natCast, Real.rpow_natCast, ← inv_pow, ← abs_inv]
-  apply (linear_inv_isBigO_right c z).abs_right.pow
+  lift k to ℕ using by lia
+  grind [(linear_inv_isBigO_right c z).abs_right.pow k,
+    zpow_natCast, Int.cast_natCast, Real.rpow_natCast, ← inv_pow, ← abs_inv]
 
 /-- For `z : ℂ` the function `c : ℤ ↦ ((c z + d) ^ k)⁻¹` is Summable for `2 ≤ k`. -/
 lemma linear_left_summable {z : ℂ} (hz : z ≠ 0) (d : ℤ) {k : ℤ} (hk : 2 ≤ k) :
@@ -231,8 +245,54 @@ lemma linear_left_summable {z : ℂ} (hz : z ≠ 0) (d : ℤ) {k : ℤ} (hk : 2
 lemma summable_linear_sub_mul_linear_add (z : ℂ) (c₁ c₂ : ℤ) :
     Summable fun n : ℤ ↦ ((c₁ * z - n) * (c₂ * z + n))⁻¹ := by
   apply summable_inv_of_isBigO_rpow_inv (a := 2) (by norm_cast)
+  simpa [pow_two] using (linear_inv_isBigO_right c₂ z).mul
+      (linear_inv_isBigO_right c₁ z).comp_neg_int
+
+lemma summable_linear_right_add_one_mul_linear_right (z : ℂ) (c₁ c₂ : ℤ) :
+    Summable fun n : ℤ ↦ ((c₁ * z + n + 1) * (c₂ * z + n))⁻¹  := by
+  apply summable_inv_of_isBigO_rpow_inv (a := 2) (by norm_cast)
+  simpa [pow_two] using (linear_inv_isBigO_right c₂ z).mul
+    (linear_inv_isBigO_right_add c₁ 1 z)
+
+lemma summable_linear_left_mul_linear_left {z : ℂ} (hz : z ≠ 0) (c₁ c₂ : ℤ) :
+    Summable fun n : ℤ ↦ ((n * z + c₁) * (n * z + c₂))⁻¹  := by
+  apply summable_inv_of_isBigO_rpow_inv (a := 2) (by norm_cast)
   simp only [Real.rpow_two, abs_mul_abs_self, pow_two]
-  simpa [sub_eq_add_neg] using (linear_inv_isBigO_right c₂ z).mul
-    (linear_inv_isBigO_right c₁ z).comp_neg_int
+  simpa using (linear_inv_isBigO_left c₂ hz).mul (linear_inv_isBigO_left c₁ hz)
+
+private lemma aux_isBigO_linear (z : ℍ) (a b : ℤ) :
+    (fun (m : Fin 2 → ℤ) ↦ ((m 0 + a : ℂ) * z + m 1 + b)⁻¹) =O[cofinite]
+    fun (m : Fin 2 → ℤ) ↦ ‖![m 0 + a, m 1 + b]‖⁻¹ := by
+  rw [Asymptotics.isBigO_iff]
+  have h0 : z ∈ verticalStrip |z.re| (z.im) := by simp [mem_verticalStrip_iff]
+  use ‖r ⟨⟨|z.re|, z.im⟩, z.2⟩‖⁻¹
+  filter_upwards with m
+  apply le_trans (by simpa [Real.rpow_neg_one, add_assoc] using
+    summand_bound_of_mem_verticalStrip zero_le_one ![m 0 + a, m 1 + b] z.2 h0)
+  simp [abs_of_pos (r_pos _)]
+  aesop
+
+lemma isLittleO_const_left_of_properSpace_of_discreteTopology
+    {α : Type*} (a : α) [NormedAddCommGroup α] [DiscreteTopology α]
+    [ProperSpace α] : (fun _ : α ↦ a) =o[cofinite] (‖·‖) := by
+  simpa [isLittleO_const_left, Function.comp_def] using
+    .inr <| tendsto_norm_comp_cofinite_atTop_of_isClosedEmbedding IsClosedEmbedding.id
+
+lemma vec_add_const_isTheta (a b : ℤ) :
+    (fun (m : Fin 2 → ℤ) => ‖![m 0 + a, m 1 + b]‖⁻¹) =Θ[cofinite] (fun m => ‖m‖⁻¹) := by
+  have (x : Fin 2 → ℤ) : ![x 0 + a, x 1 + b] = x + ![a, b] := List.ofFn_inj.mp rfl
+  simpa only [isTheta_inv, isTheta_norm_left, this] using (IsTheta.add_isLittleO
+  (by rw [← isTheta_norm_left]) (isLittleO_const_left_of_properSpace_of_discreteTopology ![a, b]))
+
+lemma isBigO_linear_add_const_vec (z : ℍ) (a b : ℤ) :
+    (fun m : (Fin 2 → ℤ) => (((m 0 : ℂ) + a) * z + m 1 + b)⁻¹) =O[cofinite] (fun m => ‖m‖⁻¹) :=
+  (aux_isBigO_linear z a b).trans (vec_add_const_isTheta a b).isBigO
+
+/-- If a function `ℤ² → ℂ` is `O (‖n‖ ^ a)⁻¹` for `2 < a`, then the function is summable. -/
+lemma summable_of_isBigO_rpow_norm {E : Type*} [NormedAddCommGroup E] [CompleteSpace E]
+    {f : (Fin 2 → ℤ) → E} {a : ℝ} (hab : 2 < a)
+    (hf : f =O[cofinite] fun n ↦ (‖n‖ ^ a)⁻¹) : Summable f :=
+  summable_of_isBigO
+    ((summable_one_div_norm_rpow hab).congr fun b ↦ Real.rpow_neg (norm_nonneg b) a) hf
 
 end EisensteinSeries

Mathlib/NumberTheory/ModularForms/Identities.lean

@@ -44,4 +44,9 @@ theorem T_zpow_width_invariant (N : ℕ) (k n : ℤ) (f : SlashInvariantForm (Ga
   rw [modular_T_zpow_smul z (N * n)]
   simpa only [Int.cast_mul, Int.cast_natCast] using vAdd_width_periodic N k n f z
 
+lemma slash_S_apply (f : ℍ → ℂ) (k : ℤ) (z : ℍ) :
+    (f ∣[k] ModularGroup.S) z = f (.mk _ z.im_inv_neg_coe_pos) * z ^ (-k) := by
+  rw [SL_slash_apply, modular_S_smul]
+  simp [ModularGroup.S, denom]
+
 end SlashInvariantForm

Mathlib/NumberTheory/TsumDivisorsAntidiagonal.lean

@@ -0,0 +1,143 @@
+/-
+Copyright (c) 2025 Chris Birkbeck. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Chris Birkbeck
+-/
+module
+
+public import Mathlib.Analysis.SpecificLimits.Normed
+public import Mathlib.NumberTheory.ArithmeticFunction.Misc
+
+
+/-!
+# Lemmas on infinite sums over the antidiagonal of the divisors function
+
+This file contains lemmas about the antidiagonal of the divisors function. It defines the map from
+`Nat.divisorsAntidiagonal n` to `ℕ+ × ℕ+` given by sending `n = a * b` to `(a, b)`.
+
+We then prove some identities about the infinite sums over this antidiagonal, such as
+`∑' n : ℕ+, n ^ k * r ^ n / (1 - r ^ n) = ∑' n : ℕ+, σ k n * r ^ n`
+which are used for Eisenstein series and their q-expansions. This is also a special case of
+Lambert series.
+
+-/
+
+@[expose] public section
+
+open Filter Complex ArithmeticFunction Nat Topology
+
+/-- The map from `Nat.divisorsAntidiagonal n` to `ℕ+ × ℕ+` given by sending `n = a * b`
+to `(a, b)`. -/
+def divisorsAntidiagonalFactors (n : ℕ+) : Nat.divisorsAntidiagonal n → ℕ+ × ℕ+ := fun x ↦
+  ⟨⟨x.1.1, Nat.pos_of_mem_divisors (Nat.fst_mem_divisors_of_mem_antidiagonal x.2)⟩,
+    (⟨x.1.2, Nat.pos_of_mem_divisors (Nat.snd_mem_divisors_of_mem_antidiagonal x.2)⟩ : ℕ+),
+    Nat.pos_of_mem_divisors (Nat.snd_mem_divisors_of_mem_antidiagonal x.2)⟩
+
+lemma divisorsAntidiagonalFactors_eq {n : ℕ+} (x : Nat.divisorsAntidiagonal n) :
+    (divisorsAntidiagonalFactors n x).1.1 * (divisorsAntidiagonalFactors n x).2.1 = n := by
+  simp [divisorsAntidiagonalFactors, (Nat.mem_divisorsAntidiagonal.mp x.2).1]
+
+lemma divisorsAntidiagonalFactors_one (x : Nat.divisorsAntidiagonal 1) :
+    (divisorsAntidiagonalFactors 1 x) = (1, 1) := by
+  have h := Nat.mem_divisorsAntidiagonal.mp x.2
+  simp only [mul_eq_one, ne_eq, one_ne_zero, not_false_eq_true, and_true] at h
+  simp [divisorsAntidiagonalFactors, h.1, h.2]
+
+/-- The equivalence from the union over `n` of `Nat.divisorsAntidiagonal n` to `ℕ+ × ℕ+`
+given by sending `n = a * b` to `(a, b)`. -/
+def sigmaAntidiagonalEquivProd : (Σ n : ℕ+, Nat.divisorsAntidiagonal n) ≃ ℕ+ × ℕ+ where
+  toFun x := divisorsAntidiagonalFactors x.1 x.2
+  invFun x :=
+    ⟨⟨x.1.val * x.2.val, mul_pos x.1.2 x.2.2⟩, ⟨x.1, x.2⟩, by simp [Nat.mem_divisorsAntidiagonal]⟩
+  left_inv := by
+    rintro ⟨n, ⟨k, l⟩, h⟩
+    rw [Nat.mem_divisorsAntidiagonal] at h
+    ext <;> simp [divisorsAntidiagonalFactors, ← PNat.coe_injective.eq_iff, h.1]
+  right_inv _ := rfl
+
+lemma sigmaAntidiagonalEquivProd_symm_apply_fst (x : ℕ+ × ℕ+) :
+    (sigmaAntidiagonalEquivProd.symm x).1 = x.1.1 * x.2.1 := rfl
+
+lemma sigmaAntidiagonalEquivProd_symm_apply_snd (x : ℕ+ × ℕ+) :
+    (sigmaAntidiagonalEquivProd.symm x).2 = (x.1.1, x.2.1) := rfl
+
+section tsum
+
+variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [NormSMulClass ℤ 𝕜]
+
+omit [NormSMulClass ℤ 𝕜] in
+lemma summable_norm_pow_mul_geometric_div_one_sub (k : ℕ) {r : 𝕜} (hr : ‖r‖ < 1) :
+    Summable fun n : ℕ ↦ n ^ k * r ^ n / (1 - r ^ n) := by
+  simp only [div_eq_mul_one_div (_ * _ ^ _)]
+  apply Summable.mul_tendsto_const (c := 1 / (1 - 0))
+    (by simpa using summable_norm_pow_mul_geometric_of_norm_lt_one k hr)
+  simpa only [Nat.cofinite_eq_atTop] using
+   tendsto_const_nhds.div ((tendsto_pow_atTop_nhds_zero_of_norm_lt_one hr).const_sub 1) (by simp)
+
+private lemma summable_divisorsAntidiagonal_aux (k : ℕ) {r : 𝕜} (hr : ‖r‖ < 1) :
+    Summable fun c : (n : ℕ+) × {x // x ∈ (n : ℕ).divisorsAntidiagonal} ↦
+    (c.2.1.2) ^ k * (r ^ (c.2.1.1 * c.2.1.2)) := by
+  apply Summable.of_norm
+  rw [summable_sigma_of_nonneg (fun a ↦ by positivity)]
+  constructor
+  · exact fun n ↦ (hasSum_fintype _).summable
+  · simp only [norm_mul, norm_pow, tsum_fintype, Finset.univ_eq_attach]
+    apply Summable.of_nonneg_of_le (f := fun c : ℕ+ ↦ ‖(c : 𝕜) ^ (k + 1) * r ^ (c : ℕ)‖)
+      (fun b ↦ Finset.sum_nonneg (fun _ _ ↦ mul_nonneg (by simp) (by simp))) (fun b ↦ ?_)
+      (by apply (summable_norm_pow_mul_geometric_of_norm_lt_one (k + 1) hr).subtype)
+    transitivity ∑ _ ∈ (b : ℕ).divisors, ‖(b : 𝕜)‖ ^ k * ‖r ^ (b : ℕ)‖
+    · rw [(b : ℕ).divisorsAntidiagonal.sum_attach (fun x ↦ ‖(x.2 : 𝕜)‖ ^ _ * _ ^ (x.1 * x.2)),
+          sum_divisorsAntidiagonal ((fun x y ↦ ‖(y : 𝕜)‖ ^ k * _ ^ (x * y)))]
+      gcongr with i hi
+      · simpa using le_of_dvd b.2 (div_dvd_of_dvd (dvd_of_mem_divisors hi))
+      · rw [norm_pow, mul_comm, Nat.div_mul_cancel (dvd_of_mem_divisors hi)]
+    · simp only [norm_pow, Finset.sum_const, nsmul_eq_mul, ← mul_assoc, add_comm k 1, pow_add,
+        pow_one, norm_mul]
+      gcongr
+      simpa using Nat.card_divisors_le_self b
+
+theorem summable_prod_mul_pow (k : ℕ) {r : 𝕜} (hr : ‖r‖ < 1) :
+    Summable fun c : (ℕ+ × ℕ+) ↦ c.2 ^ k * (r ^ (c.1 * c.2 : ℕ)) := by
+  simpa [sigmaAntidiagonalEquivProd.summable_iff.symm] using summable_divisorsAntidiagonal_aux k hr
+
+-- access notation `σ`
+open scoped sigma
+
+theorem tsum_prod_pow_eq_tsum_sigma (k : ℕ) {r : 𝕜} (hr : ‖r‖ < 1) :
+    ∑' d : ℕ+, ∑' c : ℕ+, c ^ k * r ^ (d * c : ℕ) = ∑' e : ℕ+, σ k e * r ^ (e : ℕ) := by
+  suffices ∑' c : ℕ+ × ℕ+, c.2 ^ k * r ^ (c.1 * c.2 : ℕ) =
+    ∑' e : ℕ+, σ k e * r ^ (e : ℕ) by rwa [← (summable_prod_mul_pow k hr).tsum_prod]
+  simp only [← sigmaAntidiagonalEquivProd.tsum_eq, sigmaAntidiagonalEquivProd,
+    divisorsAntidiagonalFactors, PNat.mk_coe, Equiv.coe_fn_mk, sigma_eq_sum_div, cast_sum,
+    cast_pow, Summable.tsum_sigma (summable_divisorsAntidiagonal_aux k hr)]
+  refine tsum_congr fun n ↦ ?_
+  simpa [tsum_fintype, Finset.sum_mul,
+    (n : ℕ).divisorsAntidiagonal.sum_attach fun x : ℕ × ℕ ↦ x.2 ^ k * r ^ (x.1 * x.2),
+    sum_divisorsAntidiagonal fun x y ↦ y ^ k * r ^ (x * y)]
+      using Finset.sum_congr rfl fun i hi ↦ by rw [Nat.mul_div_cancel' (dvd_of_mem_divisors hi)]
+
+lemma tsum_pow_div_one_sub_eq_tsum_sigma {r : 𝕜} (hr : ‖r‖ < 1) (k : ℕ) :
+    ∑' n : ℕ+, n ^ k * r ^ (n : ℕ) / (1 - r ^ (n : ℕ)) = ∑' n : ℕ+, σ k n * r ^ (n : ℕ) := by
+  have (m : ℕ) [NeZero m] := tsum_geometric_of_norm_lt_one (ξ := r ^ m)
+    (by simpa using pow_lt_one₀ (by simp) hr (NeZero.ne _))
+  simp only [div_eq_mul_inv, ← this, ← tsum_mul_left, mul_assoc, ← _root_.pow_succ',
+    ← fun (n : ℕ) ↦ tsum_pnat_eq_tsum_succ (f := fun m ↦ n ^ k * (r ^ n) ^ m)]
+  have h00 := tsum_prod_pow_eq_tsum_sigma k hr
+  rw [Summable.tsum_comm (by apply (summable_prod_mul_pow k hr).prod_symm)] at h00
+  rw [← h00]
+  exact tsum_congr₂ <| fun b c ↦ by simp [mul_comm c.val b.val, pow_mul]
+
+omit [CompleteSpace 𝕜] [NormSMulClass ℤ 𝕜] in
+lemma tendsto_zero_geometric_tsum_pnat {r : 𝕜} (hr : ‖r‖ < 1) :
+    Tendsto (fun m : ℕ+ ↦ ∑' n : ℕ+, r ^ (n * m : ℕ)) atTop (𝓝 0) := by
+  have h1 (m : ℕ+) : ‖r ^ (m : ℕ)‖ < 1 := by
+    rwa [norm_pow, pow_lt_one_iff_of_nonneg (norm_nonneg _) (NeZero.ne _)]
+  have h2 (m : ℕ+) : ∑' n : ℕ+, r ^ (n * m : ℕ) = (1 - r ^ (m : ℕ))⁻¹ - 1 := by
+    have := tsum_geometric_of_norm_lt_one (h1 m)
+    rw [← tsum_zero_pnat_eq_tsum_nat (summable_geometric_of_norm_lt_one (h1 m))] at this
+    simp_rw [← this, pow_zero, add_sub_cancel_left, mul_comm, pow_mul]
+  rw [funext h2, (by simp : 𝓝 (0 : 𝕜) = 𝓝 ((1 - 0)⁻¹ - 1)), tendsto_sub_const_iff,
+    tendsto_inv_iff₀ (by simp), tendsto_const_sub_iff]
+  exact (tendsto_pow_atTop_nhds_zero_of_norm_lt_one hr).comp <| tendsto_PNat_val_atTop_atTop
+
+end tsum