Documentation

Mathlib.NumberTheory.ModularForms.EisensteinSeries.MDifferentiable

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}

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

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

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