feat(Analysis/SpecialFunctions): iterated derivative of cotangent (leanprover-community#27212)

Author: CBirkbeck

Mathlib/Analysis/Complex/IntegerCompl.lean

@@ -49,4 +49,10 @@ lemma integerComplement_pow_two_ne_pow_two {x : ℂ} (hx : x ∈ ℂ_ℤ) (n : 
   have := not_exists.mp hx (-n)
   simp_all [sq_eq_sq_iff_eq_or_eq_neg, eq_comm]
 
+lemma upperHalfPlane_inter_integerComplement :
+    {z : ℂ | 0 < z.im} ∩ ℂ_ℤ = {z : ℂ | 0 < z.im} := by
+  ext z
+  simp only [Set.mem_inter_iff, Set.mem_setOf_eq, and_iff_left_iff_imp]
+  exact fun hz ↦ UpperHalfPlane.coe_mem_integerComplement ⟨z, hz⟩
+
 end Complex

Mathlib/Analysis/SpecialFunctions/Trigonometric/Cotangent.lean

@@ -3,13 +3,15 @@ Copyright (c) 2024 Chris Birkbeck. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Birkbeck
 -/
+import Mathlib.Analysis.Calculus.IteratedDeriv.WithinZpow
 import Mathlib.Analysis.Complex.UpperHalfPlane.Exp
 import Mathlib.Analysis.Complex.IntegerCompl
 import Mathlib.Analysis.Complex.LocallyUniformLimit
 import Mathlib.Analysis.PSeries
 import Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd
 import Mathlib.Analysis.NormedSpace.MultipliableUniformlyOn
 import Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
+import Mathlib.Topology.Algebra.InfiniteSum.TsumUniformlyOn
 
 /-!
 # Cotangent
@@ -18,13 +20,17 @@ This file contains lemmas about the cotangent function, including useful series
 In particular, we prove that
 `π * cot (π * z) = π * I - 2 * π * I * ∑' n : ℕ, Complex.exp (2 * π * I * z) ^ n`
 as well as the infinite sum representation of cotangent (also known as the Mittag-Leffler
-expansion): `π * cot (π * z) = 1 / z + ∑' n : ℕ+, (1 / ((z : ℂ) - n) + 1 / (z + n))`.
+expansion): `π * cot (π * z) = 1 / z + ∑' n : ℕ+, (1 / (z - n) + 1 / (z + n))`.
 -/
 
 open Real Complex
 
 open scoped UpperHalfPlane
 
+local notation "ℂ_ℤ" => integerComplement
+
+local notation "ℍₒ" => UpperHalfPlane.upperHalfPlaneSet
+
 lemma Complex.cot_eq_exp_ratio (z : ℂ) :
     cot z = (Complex.exp (2 * I * z) + 1) / (I * (1 - Complex.exp (2 * I * z))) := by
   rw [Complex.cot, Complex.sin, Complex.cos]
@@ -63,8 +69,6 @@ open Filter Function
 
 open scoped Topology BigOperators Nat Complex
 
-local notation "ℂ_ℤ" => integerComplement
-
 variable {x : ℂ} {Z : Set ℂ}
 
 /-- The main term in the infinite product for sine. -/
@@ -77,14 +81,14 @@ lemma sineTerm_ne_zero {x : ℂ} (hx : x ∈ ℂ_ℤ) (n : ℕ) : 1 + sineTerm x
     aesop
   · simp [Nat.cast_add_one_ne_zero n]
 
-theorem tendsto_euler_sin_prod' (h0 : x ≠ 0) :
+lemma tendsto_euler_sin_prod' (h0 : x ≠ 0) :
     Tendsto (fun n : ℕ ↦ ∏ i ∈ Finset.range n, (1 + sineTerm x i)) atTop
     (𝓝 (sin (π * x) / (π * x))) := by
   rw [show (sin (π * x) / (π * x)) = sin (π * x) * (1 / (π * x)) by ring]
   apply (Filter.Tendsto.mul_const (b := 1 / (π * x)) (tendsto_euler_sin_prod x)).congr
   exact fun n ↦ by field_simp; rfl
 
-theorem multipliable_sineTerm (x : ℂ) : Multipliable fun i ↦ (1 + sineTerm x i) := by
+lemma multipliable_sineTerm (x : ℂ) : Multipliable fun i ↦ (1 + sineTerm x i) := by
   apply multipliable_one_add_of_summable
   have := summable_pow_div_add (x ^ 2) 2 1 Nat.one_lt_two
   simpa [sineTerm] using this
@@ -108,46 +112,52 @@ private lemma sineTerm_bound_aux (hZ : IsCompact Z) :
     gcongr
     apply le_trans (hs x hx) (le_abs_self s)
 
-theorem multipliableUniformlyOn_euler_sin_prod_on_compact (hZC : IsCompact Z) :
+lemma multipliableUniformlyOn_euler_sin_prod_on_compact (hZC : IsCompact Z) :
     MultipliableUniformlyOn (fun n : ℕ => fun z : ℂ => (1 + sineTerm z n)) {Z} := by
   obtain ⟨u, hu, hu2⟩ := sineTerm_bound_aux hZC
   refine Summable.multipliableUniformlyOn_nat_one_add hZC hu ?_ ?_
   · filter_upwards with n z hz using hu2 n z hz
   · fun_prop
 
-theorem HasProdUniformlyOn_sineTerm_prod_on_compact (hZ2 : Z ⊆ ℂ_ℤ)
+lemma HasProdUniformlyOn_sineTerm_prod_on_compact (hZ2 : Z ⊆ ℂ_ℤ)
     (hZC : IsCompact Z) :
     HasProdUniformlyOn (fun n : ℕ => fun z : ℂ => (1 + sineTerm z n))
     (fun x => (Complex.sin (↑π * x) / (↑π * x))) {Z} := by
   apply (multipliableUniformlyOn_euler_sin_prod_on_compact hZC).hasProdUniformlyOn.congr_right
   exact fun s hs x hx => euler_sineTerm_tprod (by aesop)
 
-theorem HasProdLocallyUniformlyOn_euler_sin_prod :
+lemma HasProdLocallyUniformlyOn_euler_sin_prod :
     HasProdLocallyUniformlyOn (fun n : ℕ => fun z : ℂ => (1 + sineTerm z n))
     (fun x => (Complex.sin (π * x) / (π * x))) ℂ_ℤ := by
   apply hasProdLocallyUniformlyOn_of_forall_compact isOpen_compl_range_intCast
   exact fun _ hZ hZC => HasProdUniformlyOn_sineTerm_prod_on_compact hZ hZC
 
-theorem sin_pi_z_ne_zero (hz : x ∈ ℂ_ℤ) : Complex.sin (π * x) ≠ 0 := by
+/-- `sin π z` is non vanishing on the complement of the integers in `ℂ`. -/
+theorem sin_pi_mul_ne_zero (hx : x ∈ ℂ_ℤ) : Complex.sin (π * x) ≠ 0 := by
   apply Complex.sin_ne_zero_iff.2
   intro k
   nth_rw 2 [mul_comm]
   exact Injective.ne (mul_right_injective₀ (ofReal_ne_zero.mpr Real.pi_ne_zero)) (by aesop)
 
-theorem tendsto_logDeriv_euler_sin_div (hx : x ∈ ℂ_ℤ) :
+lemma cot_pi_mul_contDiffWithinAt (k : ℕ∞) (hx : x ∈ ℂ_ℤ) :
+  ContDiffWithinAt ℂ k (fun x ↦ (↑π * x).cot) ℍₒ x := by
+  simp_rw [Complex.cot, Complex.cos, Complex.sin]
+  exact ContDiffWithinAt.div (by fun_prop) (by fun_prop) (sin_pi_mul_ne_zero hx)
+
+lemma tendsto_logDeriv_euler_sin_div (hx : x ∈ ℂ_ℤ) :
     Tendsto (fun n : ℕ ↦ logDeriv (fun z ↦ ∏ j ∈ Finset.range n, (1 + sineTerm z j)) x)
         atTop (𝓝 <| logDeriv (fun t ↦ (Complex.sin (π * t) / (π * t))) x) := by
   refine logDeriv_tendsto (isOpen_compl_range_intCast) ⟨x, hx⟩
       HasProdLocallyUniformlyOn_euler_sin_prod.tendstoLocallyUniformlyOn_finsetRange ?_ ?_
   · filter_upwards with n using by fun_prop
   · simp only [ne_eq, div_eq_zero_iff, mul_eq_zero, ofReal_eq_zero, not_or]
-    exact ⟨sin_pi_z_ne_zero hx, Real.pi_ne_zero, integerComplement.ne_zero hx⟩
+    exact ⟨sin_pi_mul_ne_zero hx, Real.pi_ne_zero, integerComplement.ne_zero hx⟩
 
-theorem logDeriv_sin_div_eq_cot (hz : x ∈ ℂ_ℤ) :
+lemma logDeriv_sin_div_eq_cot (hz : x ∈ ℂ_ℤ) :
     logDeriv (fun t ↦ (Complex.sin (π * t) / (π * t))) x = π * cot (π * x) - 1 / x := by
   have : (fun t ↦ (Complex.sin (π * t)/ (π * t))) = fun z ↦
     (Complex.sin ∘ fun t ↦ π * t) z / (π * z) := by simp
-  rw [this, logDeriv_div _ (by apply sin_pi_z_ne_zero hz) ?_
+  rw [this, logDeriv_div _ (by apply sin_pi_mul_ne_zero hz) ?_
     (DifferentiableAt.comp _ (Complex.differentiableAt_sin) (by fun_prop)) (by fun_prop),
     logDeriv_comp (Complex.differentiableAt_sin) (by fun_prop), Complex.logDeriv_sin,
     deriv_const_mul _ (by fun_prop), deriv_id'', logDeriv_const_mul, logDeriv_id']
@@ -159,7 +169,7 @@ theorem logDeriv_sin_div_eq_cot (hz : x ∈ ℂ_ℤ) :
 /-- The term in the infinite sum expansion of cot. -/
 noncomputable abbrev cotTerm (x : ℂ) (n : ℕ) : ℂ := 1 / (x - (n + 1)) + 1 / (x + (n + 1))
 
-theorem logDeriv_sineTerm_eq_cotTerm (hx : x ∈ ℂ_ℤ) (i : ℕ) :
+lemma logDeriv_sineTerm_eq_cotTerm (hx : x ∈ ℂ_ℤ) (i : ℕ) :
     logDeriv (fun (z : ℂ) ↦ 1 + sineTerm z i) x = cotTerm x i := by
   have h1 := integerComplement_add_ne_zero hx (i + 1)
   have h2 : ((x : ℂ) - (i + 1)) ≠ 0 := by
@@ -182,7 +192,7 @@ lemma logDeriv_prod_sineTerm_eq_sum_cotTerm (hx : x ∈ ℂ_ℤ) (n : ℕ) :
   · exact fun i _ ↦ sineTerm_ne_zero hx i
   · fun_prop
 
-theorem tendsto_logDeriv_euler_cot_sub (hx : x ∈ ℂ_ℤ) :
+lemma tendsto_logDeriv_euler_cot_sub (hx : x ∈ ℂ_ℤ) :
     Tendsto (fun n : ℕ => ∑ j ∈ Finset.range n, cotTerm x j) atTop
     (𝓝 <| π * cot (π * x)- 1 / x) := by
   simp_rw [← logDeriv_sin_div_eq_cot hx, ← logDeriv_prod_sineTerm_eq_sum_cotTerm hx]
@@ -196,7 +206,7 @@ lemma cotTerm_identity (hz : x ∈ ℂ_ℤ) (n : ℕ) :
   · simpa [sub_eq_add_neg] using integerComplement_add_ne_zero hz (-(n + 1) : ℤ)
   · simpa using (integerComplement_add_ne_zero hz ((n : ℤ) + 1))
 
-theorem Summable_cotTerm (hz : x ∈ ℂ_ℤ) : Summable fun n ↦ cotTerm x n := by
+lemma Summable_cotTerm (hz : x ∈ ℂ_ℤ) : Summable fun n ↦ cotTerm x n := by
   rw [funext fun n ↦ cotTerm_identity hz n]
   apply Summable.mul_left
   suffices Summable fun i : ℕ ↦ (x - (↑i : ℂ))⁻¹ * (x + (↑i : ℂ))⁻¹ by
@@ -207,7 +217,7 @@ theorem Summable_cotTerm (hz : x ∈ ℂ_ℤ) : Summable fun n ↦ cotTerm x n :
   apply (EisensteinSeries.summable_linear_sub_mul_linear_add x 1 1).congr
   simp [mul_comm]
 
-theorem cot_series_rep' (hz : x ∈ ℂ_ℤ) : π * cot (π * x) - 1 / x =
+lemma cot_series_rep' (hz : x ∈ ℂ_ℤ) : π * cot (π * x) - 1 / x =
     ∑' n : ℕ, (1 / (x - (n + 1)) + 1 / (x + (n + 1))) := by
   rw [HasSum.tsum_eq]
   apply (Summable.hasSum_iff_tendsto_nat (Summable_cotTerm hz)).mpr
@@ -223,3 +233,171 @@ theorem cot_series_rep (hz : x ∈ ℂ_ℤ) :
   ring
 
 end MittagLeffler
+
+section iteratedDeriv
+
+open Set UpperHalfPlane
+
+open scoped Nat
+
+variable (k : ℕ)
+
+private lemma contDiffOn_inv_linear (d : ℤ) : ContDiffOn ℂ k (fun z : ℂ ↦ 1 / (z + d)) ℂ_ℤ := by
+  simpa using ContDiffOn.inv (by fun_prop) (fun x hx ↦ integerComplement_add_ne_zero hx d)
+
+lemma eqOn_iteratedDeriv_cotTerm (d : ℕ) : EqOn (iteratedDeriv k (fun z ↦ cotTerm z d))
+    (fun z ↦ (-1)^ k * k ! * ((z + (d + 1))^ (-1 - k : ℤ) + (z - (d + 1)) ^ (-1 - k : ℤ))) ℂ_ℤ := by
+  intro z hz
+  rw [← Pi.add_def, iteratedDeriv_add]
+  · have h2 := iter_deriv_inv_linear_sub k 1 ((d + 1 : ℂ))
+    have h3 := iter_deriv_inv_linear k 1 (d + 1 : ℂ)
+    simp only [one_div, one_mul, one_pow, mul_one, Int.reduceNeg, iteratedDeriv_eq_iterate] at *
+    rw [h2, h3]
+    ring
+  · simpa [sub_eq_add_neg] using (contDiffOn_inv_linear k (-(d + 1))).contDiffAt
+      ((isOpen_compl_range_intCast).mem_nhds hz)
+  · simpa using (contDiffOn_inv_linear k (d + 1)).contDiffAt
+      ((isOpen_compl_range_intCast).mem_nhds hz)
+
+lemma eqOn_iteratedDerivWithin_cotTerm_integerComplement (d : ℕ) :
+    EqOn (iteratedDerivWithin k (fun z ↦ cotTerm z d) ℂ_ℤ)
+    (fun z ↦ (-1) ^ k * k ! * ((z + (d + 1)) ^ (-1 - k : ℤ) +
+    (z - (d + 1)) ^ (-1 - k : ℤ))) ℂ_ℤ := by
+  apply Set.EqOn.trans (iteratedDerivWithin_of_isOpen isOpen_compl_range_intCast)
+  exact eqOn_iteratedDeriv_cotTerm ..
+
+lemma eqOn_iteratedDerivWithin_cotTerm_upperHalfPlaneSet (d : ℕ) :
+    EqOn (iteratedDerivWithin k (fun z ↦ cotTerm z d) ℍₒ)
+    (fun z ↦ (-1) ^ k * k ! * ((z + (d + 1)) ^ (-1 - k : ℤ) +
+    (z - (d + 1)) ^ (-1 - k : ℤ))) ℍₒ := by
+  apply Set.EqOn.trans (upperHalfPlane_inter_integerComplement ▸
+    iteratedDerivWithin_congr_right_of_isOpen (fun z ↦ cotTerm z d) k
+    isOpen_upperHalfPlaneSet (isOpen_compl_range_intCast))
+  intro z hz
+  simpa using eqOn_iteratedDerivWithin_cotTerm_integerComplement k d
+    (coe_mem_integerComplement ⟨z, hz⟩)
+
+open EisensteinSeries in
+private noncomputable abbrev cotTermUpperBound (A B : ℝ) (hB : 0 < B) (a : ℕ) :=
+  k ! * (2 * (r (⟨⟨A, B⟩, by simp [hB]⟩) ^ (-1 - k : ℤ)) * ‖((a + 1) ^ (-1 - k : ℤ) : ℝ)‖)
+
+private lemma summable_cotTermUpperBound (A B : ℝ) (hB : 0 < B) {k : ℕ} (hk : 1 ≤ k) :
+    Summable fun a : ℕ ↦ cotTermUpperBound k A B hB a := by
+  simp_rw [← mul_assoc]
+  apply Summable.mul_left
+  conv => enter [1, n]; rw [show (-1 - k : ℤ) = -(1 + k :) by omega, zpow_neg, zpow_natCast];
+          enter [1, 1, 1]; norm_cast
+  rw [summable_norm_iff, summable_nat_add_iff (f := fun n : ℕ ↦ ((n : ℝ) ^ (1 + k))⁻¹)]
+  exact summable_nat_pow_inv.mpr <| by omega
+
+open EisensteinSeries in
+private lemma iteratedDerivWithin_cotTerm_bounded_uniformly
+    {k : ℕ} (hk : 1 ≤ k) {K : Set ℂ} (hK : K ⊆ ℍₒ) (A B : ℝ) (hB : 0 < B)
+    (HABK : inclusion hK '' univ ⊆ verticalStrip A B) (n : ℕ) {a : ℂ} (ha : a ∈ K) :
+    ‖iteratedDerivWithin k (fun z ↦ cotTerm z n) ℍₒ a‖ ≤ cotTermUpperBound k A B hB n := by
+  simp only [eqOn_iteratedDerivWithin_cotTerm_upperHalfPlaneSet k n (hK ha), Complex.norm_mul,
+    norm_pow, norm_neg,norm_one, one_pow, Complex.norm_natCast, one_mul, cotTermUpperBound,
+    Int.reduceNeg, norm_zpow, Real.norm_eq_abs, two_mul, add_mul]
+  gcongr
+  have h1 := summand_bound_of_mem_verticalStrip (k := k + 1) (by norm_cast; omega) ![1, n + 1] hB
+      (z := ⟨a, (hK ha)⟩) (A := A) (by aesop)
+  have h2 := abs_norm_eq_max_natAbs_neg n ▸ (summand_bound_of_mem_verticalStrip (k := k + 1)
+    (by norm_cast; omega) ![1, -(n + 1)] hB (z := ⟨a, (hK ha)⟩) (A := A) (by aesop))
+  simp only [Fin.isValue, Matrix.cons_val_zero, Int.cast_one, coe_mk_subtype, one_mul,
+    Matrix.cons_val_one, Matrix.cons_val_fin_one, Int.cast_add, Int.cast_natCast, neg_add_rev,
+    abs_norm_eq_max_natAbs, Int.reduceNeg, Int.cast_neg, sub_eq_add_neg, ge_iff_le] at h1 h2 ⊢
+  refine le_trans (norm_add_le _ _) (add_le_add ?_ ?_) <;>
+    {simp only [Int.reduceNeg, norm_zpow]; norm_cast at h1 h2 ⊢}
+
+lemma summableLocallyUniformlyOn_iteratedDerivWithin_cotTerm {k : ℕ} (hk : 1 ≤ k) :
+    SummableLocallyUniformlyOn (fun n ↦ iteratedDerivWithin k (fun z ↦ cotTerm z n) ℍₒ) ℍₒ := by
+  apply SummableLocallyUniformlyOn_of_locally_bounded isOpen_upperHalfPlaneSet
+  intro K hK hKc
+  obtain ⟨A, B, hB, HABK⟩ := subset_verticalStrip_of_isCompact
+    ((isCompact_iff_isCompact_univ.mp hKc).image_of_continuousOn
+    (continuous_inclusion hK |>.continuousOn))
+  exact ⟨cotTermUpperBound k A B hB, summable_cotTermUpperBound A B hB hk,
+    iteratedDerivWithin_cotTerm_bounded_uniformly hk hK A B hB HABK⟩
+
+lemma differentiableOn_iteratedDerivWithin_cotTerm (n l : ℕ) :
+    DifferentiableOn ℂ (iteratedDerivWithin l (fun z ↦ cotTerm z n) ℍₒ) ℍₒ := by
+  suffices DifferentiableOn ℂ (fun z : ℂ ↦ (-1) ^ l * l ! * ((z + (n + 1)) ^ (-1 - l : ℤ) +
+    (z - (n + 1)) ^ (-1 - l : ℤ))) ℍₒ by
+    exact this.congr fun z hz ↦ eqOn_iteratedDerivWithin_cotTerm_upperHalfPlaneSet l n hz
+  apply DifferentiableOn.const_mul
+  apply DifferentiableOn.add <;> refine DifferentiableOn.zpow (by fun_prop) <| .inl fun x hx ↦ ?_
+  · simpa [add_eq_zero_iff_neg_eq'] using (UpperHalfPlane.ne_int ⟨x, hx⟩ (-(n + 1))).symm
+  · simpa [sub_eq_zero] using (UpperHalfPlane.ne_int ⟨x, hx⟩ (n + 1))
+
+private lemma aux_summable_add {k : ℕ} (hk : 1 ≤ k) (x : ℂ) :
+  Summable fun (n : ℕ) ↦ (x + (n + 1)) ^ (-1 - k : ℤ) := by
+  apply ((summable_nat_add_iff 1).mpr (summable_int_iff_summable_nat_and_neg.mp
+        (EisensteinSeries.linear_right_summable x 1 (k := k + 1) (by omega))).1).congr
+  simp [← zpow_neg, sub_eq_add_neg]
+
+private lemma aux_summable_sub {k : ℕ} (hk : 1 ≤ k) (x : ℂ) :
+  Summable fun (n : ℕ) ↦ (x - (n + 1)) ^ (-1 - k : ℤ) := by
+  apply ((summable_nat_add_iff 1).mpr (summable_int_iff_summable_nat_and_neg.mp
+        (EisensteinSeries.linear_right_summable x 1 (k := k + 1) (by omega))).2).congr
+  simp [← zpow_neg, sub_eq_add_neg]
+
+variable {z : ℂ}
+
+-- We have this auxiliary ugly version on the lhs so the the rhs looks nicer.
+private lemma aux_iteratedDeriv_tsum_cotTerm {k : ℕ} (hk : 1 ≤ k) (hz : z ∈ ℍₒ) :
+    (-1) ^ k * (k !) * z ^ (-1 - k : ℤ) + iteratedDerivWithin k
+    (fun z ↦ ∑' n : ℕ, cotTerm z n) ℍₒ z =
+    (-1) ^ k * k ! * ∑' n : ℤ, (z + n) ^ (-1 - k : ℤ) := by
+  rw [iteratedDerivWithin_tsum k isOpen_upperHalfPlaneSet hz
+    (fun t ht ↦ Summable_cotTerm (coe_mem_integerComplement ⟨t, ht⟩))
+    (fun l hl hl2 ↦ summableLocallyUniformlyOn_iteratedDerivWithin_cotTerm  hl)
+    (fun n l z hl hz ↦ (differentiableOn_iteratedDerivWithin_cotTerm n l).differentiableAt
+    (isOpen_upperHalfPlaneSet.mem_nhds hz))]
+  conv =>
+    enter [1, 2, 1, n]
+    rw [eqOn_iteratedDerivWithin_cotTerm_upperHalfPlaneSet k n (by simp [hz])]
+  rw [tsum_of_add_one_of_neg_add_one (by simpa using aux_summable_add hk z)
+    (by simpa [sub_eq_add_neg] using aux_summable_sub hk z),
+    tsum_mul_left, Summable.tsum_add (aux_summable_add hk z) (aux_summable_sub hk z)]
+  push_cast
+  ring_nf
+
+lemma iteratedDerivWithin_cot_sub_inv_eq_add_mul_tsum {k : ℕ} (hk : 1 ≤ k) (hz : z ∈ ℍₒ) :
+    iteratedDerivWithin k (fun x : ℂ ↦ π * cot (π * x) - 1 / x) ℍₒ z =
+    -(-1) ^ k * k ! * (z ^ (-1 - k : ℤ)) + (-1) ^ k * k ! * ∑' n : ℤ, (z + n) ^ (-1 - k : ℤ) := by
+  simp only [← aux_iteratedDeriv_tsum_cotTerm hk hz, one_div, neg_mul, neg_add_cancel_left]
+  refine iteratedDerivWithin_congr (fun z hz ↦ ?_) hz
+  simpa [cotTerm] using (cot_series_rep' (UpperHalfPlane.coe_mem_integerComplement ⟨z, hz⟩))
+
+private lemma iteratedDerivWithin_cot_pi_mul_sub_inv {z : ℂ} (hz : z ∈ ℍₒ) :
+    iteratedDerivWithin k (fun x : ℂ ↦ π * cot (π * x) - 1 / x) ℍₒ z =
+    (iteratedDerivWithin k (fun x : ℂ ↦ π * cot (π * x)) ℍₒ z) -
+    (-1) ^ k * k ! * (z ^ (-1 - k : ℤ)) := by
+  simp_rw [sub_eq_add_neg]
+  rw [iteratedDerivWithin_fun_add hz isOpen_upperHalfPlaneSet.uniqueDiffOn]
+  · simpa [iteratedDerivWithin_fun_neg] using iteratedDerivWithin_one_div k
+      isOpen_upperHalfPlaneSet hz
+  · exact ContDiffWithinAt.smul (by fun_prop) (cot_pi_mul_contDiffWithinAt k
+      (UpperHalfPlane.coe_mem_integerComplement ⟨z, hz⟩))
+  · simp only [one_div]
+    apply ContDiffWithinAt.neg
+    exact ContDiffWithinAt.inv (by fun_prop) (ne_zero ⟨z, hz⟩)
+
+lemma iteratedDerivWithin_cot_pi_mul_eq_mul_tsum_zpow {k : ℕ} (hk : 1 ≤ k) {z : ℂ} (hz : z ∈ ℍₒ) :
+    iteratedDerivWithin k (fun x : ℂ ↦ π * cot (π * x)) ℍₒ z =
+    (-1) ^ k * k ! * ∑' n : ℤ, (z + n) ^ (-1 - k : ℤ):= by
+  have h0 := iteratedDerivWithin_cot_pi_mul_sub_inv k hz
+  rw [iteratedDerivWithin_cot_sub_inv_eq_add_mul_tsum  hk hz, add_comm] at h0
+  rw [← add_left_inj (-(-1) ^ k * k ! * z ^ (-1 - k : ℤ)), h0]
+  ring
+
+/-- The series expansion of the iterated derivative of `π cot (π z)`. -/
+theorem iteratedDerivWithin_cot_pi_mul_eq_mul_tsum_div_pow {k : ℕ} (hk : 1 ≤ k) {z : ℂ}
+    (hz : z ∈ ℍₒ) :
+    iteratedDerivWithin k (fun x : ℂ ↦ π * cot (π * x)) ℍₒ z =
+      (-1) ^ k * k ! * ∑' n : ℤ, 1 / (z + n) ^ (k + 1) := by
+  convert iteratedDerivWithin_cot_pi_mul_eq_mul_tsum_zpow hk hz with n
+  rw [show (-1 - k : ℤ) = -(k + 1 :) by norm_cast; omega, zpow_neg_coe_of_pos _ (by omega),
+    one_div]
+
+end iteratedDeriv

Mathlib/NumberTheory/ModularForms/EisensteinSeries/Summable.lean

@@ -48,6 +48,20 @@ theorem abs_le_right_of_norm (m n : ℤ) : |m| ≤ ‖![n, m]‖ := by
   rw [Int.abs_eq_natAbs]
   exact Preorder.le_refl _
 
+lemma abs_norm_eq_max_natAbs (n : ℕ) :
+    ‖![1, (n + 1 : ℤ)]‖ = n + 1 := by
+  simp only [EisensteinSeries.norm_eq_max_natAbs, Matrix.cons_val_zero,  Matrix.cons_val_one,
+    Matrix.cons_val_fin_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, Matrix.cons_val_zero,  Matrix.cons_val_one,
+    Matrix.cons_val_fin_one]
+  norm_cast
+  simp
+
 section bounding_functions
 
 /-- Auxiliary function used for bounding Eisenstein series, defined as