DE₄ qexp

theorem DE₄_qexp (z : UpperHalfPlane) :    D E₄.toFun z = 240 * ∑' (n : ℕ+), (n : ℂ) * (ArithmeticFunction.sigma 3 n : ℂ) *      Complex.exp (2 * Real.pi * Complex.I * n * z) := by  let f : UpperHalfPlane → ℂ := fun w => ∑' n : ℕ+, (ArithmeticFunction.sigma 3 n : ℂ) *    Complex.exp (2 * π * Complex.I * (n : ℂ) * (w : ℂ))  have hE4_eq : E₄.toFun = (fun _ => 1) + (240 : ℂ) • f := by    ext w; simp only [ModularForm.toFun_eq_coe, f, Pi.add_apply, Pi.smul_apply, smul_eq_mul]    exact E₄_sigma_qexp w  have hDf : D f z = ∑' n : ℕ+, (n : ℂ) * (ArithmeticFunction.sigma 3 n : ℂ) *      Complex.exp (2 * π * Complex.I * (n : ℂ) * (z : ℂ)) := by    apply D_qexp_tsum_pnat _ z (sigma3_qexp_summable z) sigma3_qexp_deriv_bound  have hf_mdiff : MDiff f := by    have h : f = (240 : ℂ)⁻¹ • (fun w => E₄ w - 1) := by      ext w      simp only [f, Pi.smul_apply, smul_eq_mul]      rw [E₄_sigma_qexp w]      ring    rw [h]; exact (E₄.holo'.sub mdifferentiable_const).const_smul _  have hD_smul : D ((240 : ℂ) • f) z = (240 : ℂ) * D f z := by    rw [congrFun (D_smul 240 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₄.toFun z      = D ((fun _ => 1) + (240 : ℂ) • f) z := by rw [hE4_eq]    _ = D (fun _ => 1) z + D ((240 : ℂ) • f) z :=        congrFun (D_add _ _ mdifferentiable_const (hf_mdiff.const_smul _)) z    _ = _ := by rw [hD_one, hD_smul, zero_add, hDf]