Neg DE₂ qexp

theorem negDE₂_qexp (z : UpperHalfPlane) :    negDE₂ z = 24 * ∑' (n : ℕ+), (n : ℂ) * (ArithmeticFunction.sigma 1 n : ℂ) *      Complex.exp (2 * Real.pi * Complex.I * n * z) := by  simp only [negDE₂]  let f : UpperHalfPlane → ℂ := fun w => ∑' n : ℕ+, (ArithmeticFunction.sigma 1 n : ℂ) *    Complex.exp (2 * π * Complex.I * (n : ℂ) * (w : ℂ))  have hE2_eq : E₂ = (fun _ => 1) - (24 : ℂ) • f := by ext w; simpa [f] using E₂_sigma_qexp w  have hDf : D f z = ∑' n : ℕ+, (n : ℂ) * (ArithmeticFunction.sigma 1 n : ℂ) *      Complex.exp (2 * π * Complex.I * (n : ℂ) * (z : ℂ)) :=    D_qexp_tsum_pnat _ z (sigma1_qexp_summable z) sigma1_qexp_deriv_bound  have hf_mdiff : MDiff f := by    have h : f = (24 : ℂ)⁻¹ • (fun w => 1 - E₂ w) := by      ext w      simp only [f, Pi.smul_apply, smul_eq_mul]      rw [E₂_sigma_qexp w]      ring    rw [h]; exact (mdifferentiable_const.sub E₂_holo').const_smul _  have hD_smul : D ((24 : ℂ) • f) z = (24 : ℂ) * D f z := by    rw [congrFun (D_smul 24 f hf_mdiff) z, Pi.smul_apply, smul_eq_mul]  have hD_one : D (fun _ : UpperHalfPlane => (1 : ℂ)) z = 0 := congrFun (D_const 1) z  calc -(D E₂) z      = -(D ((fun _ => 1) - (24 : ℂ) • f)) z := by rw [hE2_eq]    _ = -(D (fun _ => 1) z - D ((24 : ℂ) • f) z) := by        rw [congrFun (D_sub _ _ mdifferentiable_const (hf_mdiff.const_smul _)) z]; rfl    _ = _ := by rw [hD_one, hD_smul, hDf]; ring