D diff qexp

theorem D_diff_qexp (z : ℍ) :    D (E₂ * E₄ - E₆) z =      720 * ∑' n : ℕ+, (↑↑n : ℂ) ^ 2 * ↑((ArithmeticFunction.sigma 3) ↑n) *        cexp (2 * ↑Real.pi * Complex.I * ↑n * z) := by  let a : ℕ+ → ℂ := fun n ↦ ↑n * ↑(σ 3 n)  let b : ℕ+ → ℂ := fun n ↦ 720 * a n  have hsum : Summable (fun n : ℕ+ => a n * cexp (2 * π * I * ↑n * ↑z)) := by    simpa [pow_one] using sigma_qexp_summable_generic 1 3 z  have hsum_deriv := qexp_deriv_bound_of_coeff_bound (a := a) fun n => by    simp only [a, Complex.norm_mul, Complex.norm_natCast]    calc (n : ℝ) * ↑(σ 3 ↑n)        ≤ (n : ℝ) * (n : ℝ)^4 := by          gcongr; exact_mod_cast ArithmeticFunction.sigma_le_pow_succ 3 n      _ = (n : ℝ)^5 := by ring  have h_eq' : ∀ w : ℍ, E₂ w * E₄ w - E₆ w =      ∑' (n : ℕ+), b n * cexp (2 * π * I * ↑n * w) := fun w => by    rw [E₂_mul_E₄_sub_E₆]    simp only [b, a, ← tsum_mul_left]    congr 1    funext n    ring  have hsum' : Summable (fun n : ℕ+ => b n * cexp (2 * π * I * ↑n * ↑z)) := by    have hterm :        (fun n : ℕ+ => b n * cexp (2 * π * I * ↑n * ↑z)) =          fun n : ℕ+ => 720 * (a n * cexp (2 * π * I * ↑n * ↑z)) := by      funext n      simp only [a, b]      ring    rw [hterm]    exact hsum.mul_left 720  have hsum_deriv' : ∀ K : Set ℂ, K ⊆ {w : ℂ | 0 < w.im} → IsCompact K →      ∃ u : ℕ+ → ℝ, Summable u ∧ ∀ (n : ℕ+) (k : K), ‖b n * (2 * π * I * ↑n) *        cexp (2 * π * I * ↑n * k.1)‖ ≤ u n := fun K hK_sub hK_compact => by    obtain ⟨u, hu_sum, hu_bound⟩ := hsum_deriv K hK_sub hK_compact    refine ⟨fun n => 720 * u n, hu_sum.mul_left 720, fun n k => ?_⟩    calc ‖b n * (2 * π * I * ↑n) * cexp (2 * π * I * ↑n * k.1)‖        = 720 * ‖a n * (2 * π * I * ↑n) * cexp (2 * π * I * ↑n * k.1)‖ := by          simp only [b, norm_mul, Complex.norm_ofNat]; ring      _ ≤ 720 * u n := mul_le_mul_of_nonneg_left (hu_bound n k) (by norm_num)  calc D (E₂ * E₄ - E₆) z      = D (fun w => ∑' (n : ℕ+), b n * cexp (2 * π * I * ↑n * w)) z := by        congr 1        ext w        exact h_eq' w    _ = ∑' (n : ℕ+), (n : ℂ) * b n * cexp (2 * π * I * ↑n * z) :=        D_qexp_tsum_pnat b z hsum' hsum_deriv'    _ = 720 * ∑' (n : ℕ+), (n : ℂ) ^ 2 * ↑(σ 3 n) * cexp (2 * π * I * ↑n * z) := by        simp only [b, a, ← tsum_mul_left, sq]        congr 1        funext n        ring