diff --git a/Mathlib.lean b/Mathlib.lean index f1a94bcde17f0a..70d09a3aa8370c 100644 --- a/Mathlib.lean +++ b/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 @@ -4884,6 +4885,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 diff --git a/Mathlib/Analysis/Complex/Exponential.lean b/Mathlib/Analysis/Complex/Exponential.lean index 29663f07f5204f..b96ee41e85ccb6 100644 --- a/Mathlib/Analysis/Complex/Exponential.lean +++ b/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] diff --git a/Mathlib/Analysis/Complex/SummableUniformlyOn.lean b/Mathlib/Analysis/Complex/SummableUniformlyOn.lean new file mode 100644 index 00000000000000..e1f9c06431aba4 --- /dev/null +++ b/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 diff --git a/Mathlib/Analysis/Normed/Module/FiniteDimension.lean b/Mathlib/Analysis/Normed/Module/FiniteDimension.lean index 7eab1928dd2c39..7e22f92c6f7d3d 100644 --- a/Mathlib/Analysis/Normed/Module/FiniteDimension.lean +++ b/Mathlib/Analysis/Normed/Module/FiniteDimension.lean @@ -9,6 +9,7 @@ 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 @@ -16,6 +17,7 @@ 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 := diff --git a/Mathlib/NumberTheory/LSeries/RiemannZeta.lean b/Mathlib/NumberTheory/LSeries/RiemannZeta.lean index 4bc1a08026084c..3b57258f4f3149 100644 --- a/Mathlib/NumberTheory/LSeries/RiemannZeta.lean +++ b/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 diff --git a/Mathlib/NumberTheory/ModularForms/EisensteinSeries/Defs.lean b/Mathlib/NumberTheory/ModularForms/EisensteinSeries/Defs.lean index 0492bdd9066ac6..1978290a11231e 100644 --- a/Mathlib/NumberTheory/ModularForms/EisensteinSeries/Defs.lean +++ b/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 diff --git a/Mathlib/NumberTheory/ModularForms/EisensteinSeries/QExpansion.lean b/Mathlib/NumberTheory/ModularForms/EisensteinSeries/QExpansion.lean new file mode 100644 index 00000000000000..f5fbe039213d4a --- /dev/null +++ b/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