Add q-expansion identities for Eisenstein series. (leanprover-community#27844)

This is PR contains some q-expansion identities that are needed to give the q-expansions of Eisenstein series, which will be added as part of  leanprover-community#27606.

Author: CBirkbeck

Mathlib.lean

@@ -1592,6 +1592,7 @@ import Mathlib.Analysis.Complex.ReImTopology
 import Mathlib.Analysis.Complex.RealDeriv
 import Mathlib.Analysis.Complex.RemovableSingularity
 import Mathlib.Analysis.Complex.Schwarz
+import Mathlib.Analysis.Complex.SummableUniformlyOn
 import Mathlib.Analysis.Complex.TaylorSeries
 import Mathlib.Analysis.Complex.Tietze
 import Mathlib.Analysis.Complex.Trigonometric
@@ -4890,6 +4891,7 @@ import Mathlib.NumberTheory.ModularForms.EisensteinSeries.Basic
 import Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
 import Mathlib.NumberTheory.ModularForms.EisensteinSeries.IsBoundedAtImInfty
 import Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable
+import Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
 import Mathlib.NumberTheory.ModularForms.EisensteinSeries.Summable
 import Mathlib.NumberTheory.ModularForms.EisensteinSeries.UniformConvergence
 import Mathlib.NumberTheory.ModularForms.Identities

Mathlib/Analysis/Complex/Exponential.lean

@@ -141,6 +141,11 @@ theorem exp_sum {α : Type*} (s : Finset α) (f : α → ℂ) :
 lemma exp_nsmul (x : ℂ) (n : ℕ) : exp (n • x) = exp x ^ n :=
   @MonoidHom.map_pow (Multiplicative ℂ) ℂ _ _  expMonoidHom _ _
 
+/-- This is a useful version of `exp_nsmul` for q-expansions of modular forms. -/
+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/Complex/SummableUniformlyOn.lean

@@ -0,0 +1,27 @@
+/-
+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.Analysis.CStarAlgebra.Classes
+import Mathlib.Analysis.Complex.LocallyUniformLimit
+import Mathlib.Topology.Algebra.InfiniteSum.UniformOn
+
+/-!
+# Differentiability of uniformly convergent series sums of functions
+
+We collect some results about the differentiability of infinite sums.
+
+-/
+
+lemma SummableLocallyUniformlyOn.differentiableOn {ι E : Type*} [NormedAddCommGroup E]
+    [NormedSpace ℂ E] [CompleteSpace E] {f : ι → ℂ → E} {s : Set ℂ}
+    (hs : IsOpen s) (h : SummableLocallyUniformlyOn (fun n ↦ ((fun z ↦ f n z))) s)
+    (hf2 : ∀ n r, r ∈ s → DifferentiableAt ℂ (f n) r) :
+    DifferentiableOn ℂ (fun z ↦ ∑' n , f n z) s := by
+  obtain ⟨g, hg⟩ := h
+  have hc := (hasSumLocallyUniformlyOn_iff_tendstoLocallyUniformlyOn.mp hg).differentiableOn ?_ hs
+  · apply hc.congr
+    apply hg.tsum_eqOn
+  · filter_upwards with t r hr using
+      DifferentiableWithinAt.fun_sum fun a ha ↦ (hf2 a r hr).differentiableWithinAt

Mathlib/Analysis/Normed/Module/FiniteDimension.lean

@@ -9,13 +9,15 @@ import Mathlib.Analysis.Normed.Affine.Isometry
 import Mathlib.Analysis.Normed.Operator.NormedSpace
 import Mathlib.Analysis.NormedSpace.RieszLemma
 import Mathlib.Analysis.Normed.Module.Ball.Pointwise
+import Mathlib.Analysis.SpecificLimits.Normed
 import Mathlib.Logic.Encodable.Pi
 import Mathlib.Topology.Algebra.AffineSubspace
 import Mathlib.Topology.Algebra.Module.FiniteDimension
 import Mathlib.Topology.Algebra.InfiniteSum.Module
 import Mathlib.Topology.Instances.Matrix
 import Mathlib.LinearAlgebra.Dimension.LinearMap
 
+
 /-!
 # Finite-dimensional normed spaces over complete fields
 
@@ -675,6 +677,29 @@ theorem summable_of_isBigO_nat' {E F : Type*} [NormedAddCommGroup E] [CompleteSp
     (hg : Summable g) (h : f =O[atTop] g) : Summable f :=
   summable_of_isBigO_nat hg.norm h.norm_right
 
+
+open Nat Asymptotics in
+/-- This is a version of `summable_norm_mul_geometric_of_norm_lt_one` for more general codomains. We
+keep the original one due to import restrictions. -/
+theorem summable_norm_mul_geometric_of_norm_lt_one' {F : Type*} [NormedRing F]
+    [NormOneClass F] [NormMulClass F] {k : ℕ} {r : F} (hr : ‖r‖ < 1) {u : ℕ → F}
+    (hu : u =O[atTop] fun n ↦ ((n ^ k : ℕ) : F)) : Summable fun n : ℕ ↦ ‖u n * r ^ n‖ := by
+  rcases exists_between hr with ⟨r', hrr', h⟩
+  apply summable_of_isBigO_nat (summable_geometric_of_lt_one ((norm_nonneg _).trans hrr'.le) h).norm
+  calc
+  fun n ↦ ‖(u n) * r ^ n‖
+  _ =O[atTop] fun n ↦ ‖u n‖ * ‖r‖ ^ n := by
+      apply (IsBigOWith.of_bound (c := ‖(1 : ℝ)‖) ?_).isBigO
+      filter_upwards [eventually_norm_pow_le r] with n hn
+      simp
+  _ =O[atTop] fun n ↦ ‖((n : F) ^ k)‖ * ‖r‖ ^ n := by
+      simpa [Nat.cast_pow] using
+      (isBigO_norm_left.mpr (isBigO_norm_right.mpr hu)).mul (isBigO_refl (fun n ↦ (‖r‖ ^ n)) atTop)
+  _ =O[atTop] fun n ↦ ‖r' ^ n‖ := by
+      convert isBigO_norm_right.mpr (isBigO_norm_left.mpr
+        (isLittleO_pow_const_mul_const_pow_const_pow_of_norm_lt k hrr').isBigO)
+      simp only [norm_pow, norm_mul]
+
 theorem summable_of_isEquivalent {ι E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
     [FiniteDimensional ℝ E] {f : ι → E} {g : ι → E} (hg : Summable g) (h : f ~[cofinite] g) :
     Summable f :=

Mathlib/NumberTheory/LSeries/RiemannZeta.lean

@@ -197,6 +197,17 @@ theorem zeta_nat_eq_tsum_of_gt_one {k : ℕ} (hk : 1 < k) :
       (by rwa [← ofReal_natCast, ofReal_re, ← Nat.cast_one, Nat.cast_lt] : 1 < re k),
     cpow_natCast]
 
+lemma two_mul_riemannZeta_eq_tsum_int_inv_pow_of_even {k : ℕ} (hk : 2 ≤ k) (hk2 : Even k) :
+    2 * riemannZeta k = ∑' (n : ℤ), ((n : ℂ) ^ k)⁻¹ := by
+  have hkk : 1 < k := by linarith
+  rw [tsum_int_eq_zero_add_two_mul_tsum_pnat]
+  · have h0 : (0 ^ k : ℂ)⁻¹ = 0 := by simp; omega
+    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]
+  · 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. -/
 lemma riemannZeta_residue_one : Tendsto (fun s ↦ (s - 1) * riemannZeta s) (𝓝[≠] 1) (𝓝 1) := by
   exact hurwitzZetaEven_residue_one 0

Mathlib/NumberTheory/ModularForms/EisensteinSeries/Defs.lean

@@ -120,6 +120,10 @@ lemma gammaSet_eq_gcd_mul_divIntMap {r : ℕ} {v : Fin 2 → ℤ} (hv : v ∈ ga
 def gammaSetDivGcdEquiv (r : ℕ) [NeZero r] : gammaSet 1 r 0 ≃ gammaSet 1 1 0 :=
     Set.BijOn.equiv _ (gammaSet_div_gcd_to_gammaSet10_bijection r)
 
+@[simp]
+lemma gammaSetDivGcdEquiv_eq (r : ℕ) [NeZero r] (v : gammaSet 1 r 0) :
+    (gammaSetDivGcdEquiv r) v = divIntMap r v.1 := rfl
+
 /-- The equivalence between `(Fin 2 → ℤ)` and `Σ n : ℕ, gammaSet 1 n 0)` . -/
 def gammaSetDivGcdSigmaEquiv : (Fin 2 → ℤ) ≃ (Σ r : ℕ, gammaSet 1 r 0) := by
   apply (Equiv.sigmaFiberEquiv finGcdMap).symm.trans

Mathlib/NumberTheory/ModularForms/EisensteinSeries/QExpansion.lean

@@ -0,0 +1,183 @@
+/-
+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.Analysis.Complex.SummableUniformlyOn
+import Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
+
+/-!
+# Einstein series q-expansions
+
+We give some identities for q-expansions of Eisenstein series that will be used in describing their
+q-expansions.
+
+-/
+
+open Set Metric TopologicalSpace Function Filter Complex EisensteinSeries
+
+open _root_.UpperHalfPlane hiding I
+
+open scoped Topology Real Nat Complex Pointwise
+
+local notation "ℍₒ" => upperHalfPlaneSet
+
+private lemma iteratedDerivWithin_cexp_aux (k m : ℕ) (p : ℝ) {S : Set ℂ} (hs : IsOpen S) :
+    EqOn (iteratedDerivWithin k (fun s : ℂ ↦ cexp (2 * π * I * m * s / p)) S)
+    (fun s ↦ (2 * π * I * m / p) ^ k * cexp (2 * π * I * m * s / p)) S := by
+  apply EqOn.trans (iteratedDerivWithin_of_isOpen hs)
+  intro x hx
+  have : (fun s ↦ cexp (2 * π * I * m * s / p)) = fun s ↦ cexp (((2 * π * I * m) / p) * s) := by
+    ext z
+    ring_nf
+  simp only [this, iteratedDeriv_cexp_const_mul]
+  ring_nf
+
+private lemma aux_IsBigO_mul (k l : ℕ) (p : ℝ) {f : ℕ → ℂ}
+    (hf : f =O[atTop] fun n ↦ ((n ^ l) : ℝ)) :
+    (fun n ↦ f n * (2 * π * I * n / p) ^ k) =O[atTop] fun n ↦ (↑(n ^ (l + k)) : ℝ) := by
+  have h0 : (fun n : ℕ ↦ (2 * π * I * n / p) ^ k) =O[atTop] fun n ↦ ((n ^ k) : ℝ) := by
+    have h1 : (fun n : ℕ ↦ (2 * π * I * n / p) ^ k) =
+        fun n : ℕ ↦ ((2 * π * I / p) ^ k) * n ^ k := by
+      ext z
+      ring
+    simpa [h1] using isBigO_ofReal_right.mp (Asymptotics.isBigO_const_mul_self
+      ((2 * π * I / p) ^ k) (fun (n : ℕ) ↦ (↑(n ^ k) : ℝ)) atTop)
+  simp only [Nat.cast_pow]
+  convert hf.mul h0
+  ring
+
+open BoundedContinuousFunction in
+/-- The infinte sum of `k`-th iterated derivative of the complex exponential multiplied by a
+function that grows polynomially is absolutely and uniformly convergent. -/
+theorem summableLocallyUniformlyOn_iteratedDerivWithin_smul_cexp (k l : ℕ) {f : ℕ → ℂ} {p : ℝ}
+    (hp : 0 < p) (hf : f =O[atTop] (fun n ↦ ((n ^ l) : ℝ))) :
+    SummableLocallyUniformlyOn (fun n ↦ (f n) •
+      iteratedDerivWithin k (fun z ↦ cexp (2 * π * I * z / p) ^ n) ℍₒ) ℍₒ := by
+  apply SummableLocallyUniformlyOn_of_locally_bounded isOpen_upperHalfPlaneSet
+  intro K hK hKc
+  have : CompactSpace K := isCompact_univ_iff.mp (isCompact_iff_isCompact_univ.mp hKc)
+  let c : ContinuousMap K ℂ := ⟨fun r : K ↦ Complex.exp (2 * π * I * r / p), by fun_prop⟩
+  let r : ℝ := ‖mkOfCompact c‖
+  have hr : ‖r‖ < 1 := by
+    simp only [norm_norm, r, norm_lt_iff_of_compact Real.zero_lt_one, mkOfCompact_apply,
+      ContinuousMap.coe_mk, c]
+    intro x
+    have h1 : cexp (2 * π * I * (x / p)) = cexp (2 * π * I * x / p) := by
+      ring_nf
+    simpa using h1 ▸ norm_exp_two_pi_I_lt_one ⟨((x : ℂ) / p), by aesop⟩
+  refine ⟨_, by simpa using (summable_norm_mul_geometric_of_norm_lt_one' hr
+    (Asymptotics.isBigO_norm_left.mpr (aux_IsBigO_mul k l p hf))), fun n z hz ↦ ?_⟩
+  have h0 := pow_le_pow_left₀ (norm_nonneg _) (norm_coe_le_norm (mkOfCompact c) ⟨z, hz⟩) n
+  simp only [norm_mkOfCompact, mkOfCompact_apply, ContinuousMap.coe_mk, ← exp_nsmul', Pi.smul_apply,
+    iteratedDerivWithin_cexp_aux k n p isOpen_upperHalfPlaneSet (hK hz), smul_eq_mul,
+    norm_mul, norm_pow, Complex.norm_div, norm_ofNat, norm_real, Real.norm_eq_abs, norm_I, mul_one,
+    norm_natCast, abs_norm, ge_iff_le, r, c] at *
+  rw [← mul_assoc]
+  gcongr
+  convert h0
+  rw [← norm_pow, ← exp_nsmul']
+
+/-- This is a version of `summableLocallyUniformlyOn_iteratedDerivWithin_smul_cexp` for level one
+and q-expansion coefficients all `1`. -/
+theorem summableLocallyUniformlyOn_iteratedDerivWithin_cexp (k : ℕ) :
+    SummableLocallyUniformlyOn
+      (fun n ↦ iteratedDerivWithin k (fun z ↦ cexp (2 * π * I * z) ^ n) ℍₒ) ℍₒ := by
+  have h0 : (fun n : ℕ ↦ (1 : ℂ)) =O[atTop] fun n ↦ ((n ^ 1) : ℝ) := by
+    simp only [Asymptotics.isBigO_iff, norm_one, norm_pow, Real.norm_natCast,
+      eventually_atTop, ge_iff_le]
+    exact ⟨1, 1, fun b hb ↦ by norm_cast; simp [hb]⟩
+  simpa using summableLocallyUniformlyOn_iteratedDerivWithin_smul_cexp k 1 (p := 1)
+    (by norm_num) h0
+
+lemma differentiableAt_iteratedDerivWithin_cexp (n a : ℕ) {s : Set ℂ} (hs : IsOpen s)
+    {r : ℂ} (hr : r ∈ s) : DifferentiableAt ℂ
+      (iteratedDerivWithin a (fun z ↦ cexp (2 * π * I * z) ^ n) s) r := by
+  apply DifferentiableOn.differentiableAt _ (hs.mem_nhds hr)
+  suffices DifferentiableOn ℂ (iteratedDeriv a (fun z ↦ cexp (2 * π * I * z) ^ n)) s by
+    apply this.congr (iteratedDerivWithin_of_isOpen hs)
+  fun_prop
+
+lemma iteratedDerivWithin_tsum_cexp_eq (k : ℕ) (z : ℍ) :
+    iteratedDerivWithin k (fun z ↦ ∑' n : ℕ, cexp (2 * π * I * z) ^ n) ℍₒ z =
+    ∑' n : ℕ, iteratedDerivWithin k (fun s : ℂ ↦ cexp (2 * π * I * s) ^ n) ℍₒ z := by
+  rw [iteratedDerivWithin_tsum k isOpen_upperHalfPlaneSet (by simpa using z.2)]
+  · exact fun x hx ↦ summable_geometric_iff_norm_lt_one.mpr
+      (UpperHalfPlane.norm_exp_two_pi_I_lt_one ⟨x, hx⟩)
+  · exact fun n _ _ ↦ summableLocallyUniformlyOn_iteratedDerivWithin_cexp n
+  · exact fun n l z hl hz ↦ differentiableAt_iteratedDerivWithin_cexp n l
+      isOpen_upperHalfPlaneSet hz
+
+lemma contDiffOn_tsum_cexp (k : ℕ∞) :
+    ContDiffOn ℂ k (fun z : ℂ ↦ ∑' n : ℕ, cexp (2 * π * I * z) ^ n) ℍₒ :=
+  contDiffOn_of_differentiableOn_deriv fun m _ z hz ↦
+  (((summableLocallyUniformlyOn_iteratedDerivWithin_cexp m).differentiableOn
+  isOpen_upperHalfPlaneSet (fun n _ hz ↦ differentiableAt_iteratedDerivWithin_cexp n m
+  isOpen_upperHalfPlaneSet hz)) z hz).congr (fun z hz ↦ iteratedDerivWithin_tsum_cexp_eq m ⟨z, hz⟩)
+  (iteratedDerivWithin_tsum_cexp_eq m ⟨z, hz⟩)
+
+private lemma iteratedDerivWithin_tsum_exp_aux_eq {k : ℕ} (hk : 1 ≤ k) (z : ℍ) :
+    iteratedDerivWithin k (fun z ↦ ((π * I) -
+    (2 * π * I) * ∑' n : ℕ, cexp (2 * π * I * z) ^ n)) ℍₒ z =
+    -(2 * π * I) ^ (k + 1) * ∑' n : ℕ, n ^ k * cexp (2 * π * I * z) ^ n := by
+  have : iteratedDerivWithin k (fun z ↦ ((π * I) -
+    (2 * π * I) * ∑' n : ℕ, cexp (2 * π * I * z) ^ n)) ℍₒ z =
+    -(2 * π * I) * ∑' n : ℕ, iteratedDerivWithin k (fun s : ℂ ↦ cexp (2 * π * I * s) ^ n) ℍₒ z := by
+    rw [iteratedDerivWithin_const_sub hk, iteratedDerivWithin_fun_neg,
+      iteratedDerivWithin_const_mul (by simpa using z.2) (isOpen_upperHalfPlaneSet.uniqueDiffOn)]
+    · simp only [iteratedDerivWithin_tsum_cexp_eq, neg_mul]
+    · exact (contDiffOn_tsum_cexp k).contDiffWithinAt (by simpa using z.2)
+  have h : -(2 * π * I * (2 * π * I) ^ k) * ∑' (n : ℕ), n ^ k * cexp (2 * π * I * z) ^ n =
+        -(2 * π * I) * ∑' n : ℕ, (2 * π * I * n) ^ k * cexp (2 * π * I * z) ^ n := by
+    simp_rw [← tsum_mul_left]
+    congr
+    ext y
+    ring
+  simp only [this, neg_mul, pow_succ', h, neg_inj, mul_eq_mul_left_iff, mul_eq_zero,
+    OfNat.ofNat_ne_zero, ofReal_eq_zero, Real.pi_ne_zero, or_self, I_ne_zero, or_false]
+  congr
+  ext n
+  have := exp_nsmul' (p := 1) (a := 2 * π * I) (n := n)
+  simp_rw [div_one] at this
+  simpa [this, UpperHalfPlane.coe] using
+    iteratedDerivWithin_cexp_aux k n 1 isOpen_upperHalfPlaneSet z.2
+
+/-- This is one key identity relating infinite series to q-expansions which shows that
+`∑' n, 1 / (z + n) ^ (k + 1) = ((-2 π I) ^ (k + 1) / k !) * ∑' n, n ^ k q ^n` where
+`q = cexp (2 π I z)`. -/
+theorem EisensteinSeries.qExpansion_identity {k : ℕ} (hk : 1 ≤ k) (z : ℍ) :
+    ∑' n : ℤ, 1 / ((z : ℂ) + n) ^ (k + 1) = ((-2 * π * I) ^ (k + 1) / k !) *
+    ∑' n : ℕ, n ^ k * cexp (2 * π * I * z) ^ n := by
+  have : (-1) ^ k * k ! * ∑' n : ℤ, 1 / ((z : ℂ) + n) ^ (k + 1) =
+    -(2 * π * I) ^ (k + 1) * ∑' n : ℕ, n ^ k * cexp (2 * π * I * z) ^ n := by
+    rw [← iteratedDerivWithin_tsum_exp_aux_eq hk z,
+      ← iteratedDerivWithin_cot_pi_mul_eq_mul_tsum_div_pow hk (by simpa using z.2)]
+    exact iteratedDerivWithin_congr (fun x hx ↦ by (simpa using pi_mul_cot_pi_q_exp ⟨x, hx⟩))
+      (by simpa using z.2)
+  simp_rw [(eq_inv_mul_iff_mul_eq₀ (by simp [Nat.factorial_ne_zero])).mpr this, ← tsum_mul_left]
+  congr
+  ext n
+  rw [show (-2 * π * I) ^ (k + 1) = (-1) ^ (k + 1) * (2 * π * I) ^ (k + 1) by rw [← neg_pow]; ring]
+  field_simp
+  ring_nf
+  simp [Nat.mul_two]
+
+lemma summable_pow_mul_cexp (k : ℕ) (e : ℕ+) (z : ℍ) :
+    Summable fun c : ℕ ↦ (c : ℂ) ^ k * cexp (2 * π * I * e * z) ^ c := by
+  have he : 0 < (e * (z : ℂ)).im := by
+    simpa using z.2
+  apply ((summableLocallyUniformlyOn_iteratedDerivWithin_smul_cexp 0 k (p := 1)
+    (f := fun n ↦ (n ^ k : ℂ)) (by norm_num)
+    (by simp [← Complex.isBigO_ofReal_right, Asymptotics.isBigO_refl])).summable he).congr
+  grind [ofReal_one, iteratedDerivWithin_zero, Pi.smul_apply, smul_eq_mul]
+
+/-- This is a version of `EisensteinSeries.qExpansion_identity` for positive naturals,
+which shows that  `∑' n, 1 / (z + n) ^ (k + 1) = ((-2 π I) ^ (k + 1) / k !) * ∑' n : ℕ+, n ^ k q ^n`
+where `q = cexp (2 π I z)`. -/
+theorem EisensteinSeries.qExpansion_identity_pnat {k : ℕ} (hk : 1 ≤ k) (z : ℍ) :
+    ∑' n : ℤ, 1 / ((z : ℂ) + n) ^ (k + 1) = ((-2 * π * I) ^ (k + 1) / k !) *
+    ∑' n : ℕ+, n ^ k * cexp (2 * π * I * z) ^ (n : ℕ) := by
+  rw [EisensteinSeries.qExpansion_identity hk z, ← tsum_zero_pnat_eq_tsum_nat]
+  · simp [show k ≠ 0 by grind]
+  · apply (summable_pow_mul_cexp k 1 z).congr
+    simp