Holomorphicity of Eisenstein series

We show that Eisenstein series of weight k and level Γ(N) with congruence condition a : Fin 2 → ZMod N are holomorphic on the upper half plane, which is stated as being MDifferentiable.

theorem EisensteinSeries.div_linear_zpow_differentiableOn (k : ℤ) (a : Fin 2 → ℤ) : DifferentiableOn ℂ (fun (z : ℂ) => (↑(a 0) * z + ↑(a 1)) ^ (-k)) {z : ℂ | 0 < z.im}

Auxiliary lemma showing that for any k : ℤ the function z → 1/(c*z+d)^k is differentiable on {z : ℂ | 0 < z.im}.

theorem EisensteinSeries.eisSummand_extension_differentiableOn (k : ℤ) (a : Fin 2 → ℤ) : DifferentiableOn ℂ (EisensteinSeries.eisSummand k a ∘ ↑UpperHalfPlane.ofComplex) {z : ℂ | 0 < z.im}

Auxiliary lemma showing that for any k : ℤ and (a : Fin 2 → ℤ) the extension of eisSummand is differentiable on {z : ℂ | 0 < z.im}.

theorem EisensteinSeries.eisensteinSeries_SIF_MDifferentiable {k : ℤ} {N : ℕ} (hk : 3 ≤ k) (a : Fin 2 → ZMod N) : MDifferentiable (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⇑(EisensteinSeries.eisensteinSeries_SIF a k)

Eisenstein series are MDifferentiable (i.e. holomorphic functions from ℍ → ℂ).