Holomorphicity of E₂ and φ₀ on the upper half-plane

E₂ is holomorphic because E₂ = (πI/12)⁻¹ · logDeriv(η) where η is the Dedekind eta function. Since η is holomorphic and nonvanishing on ℍ, logDeriv(η) is holomorphic, hence E₂ is holomorphic.

theorem dedekindEtaFun'_differentiableOn : DifferentiableOn ℂ dedekindEtaFun' {z : ℂ | 0 < z.im}

The Dedekind eta function is differentiable on ℍ (as a function ℂ → ℂ).

theorem dedekindEtaFun'_ne_zero_of_im_pos {z : ℂ} (hz : 0 < z.im) : dedekindEtaFun' z ≠ 0

The Dedekind eta function is nonzero on ℍ.

theorem logDeriv_eta_differentiableOn : DifferentiableOn ℂ (logDeriv dedekindEtaFun') {z : ℂ | 0 < z.im}

logDeriv(η) is differentiable on ℍ.

theorem E₂_differentiableOn : DifferentiableOn ℂ (E₂ ∘ ↑UpperHalfPlane.ofComplex) {z : ℂ | 0 < z.im}

E₂ is holomorphic on the upper half-plane. Proof: logDeriv(η) = (π·I/12) · E₂ by eta_logDeriv', so E₂ = (π·I/12)⁻¹ · logDeriv(η) is holomorphic.