English
Eisenstein series in the SlashInvariantForm SIF is MDifferentiable (holomorphic) as a function on the upper half-plane for hk ≥ 3.
Русский
Серия Эйзенштейна в форме SlashInvariantForm SIF является комплексно-дифференцируемой (голо́морфной) на верхней полуплоскости при hk ≥ 3.
LaTeX
$$$\text{MDifferentiable}_{\mathcal{I}(\mathbb{C}) \to \mathcal{I}(\mathbb{C})}( \mathrm{eisensteinSeries\_SIF}(a,k) ).$$$
Lean4
/-- Eisenstein series are MDifferentiable (i.e. holomorphic functions from `ℍ → ℂ`). -/
theorem eisensteinSeries_SIF_MDifferentiable {k : ℤ} {N : ℕ} (hk : 3 ≤ k) (a : Fin 2 → ZMod N) :
MDifferentiable 𝓘(ℂ) 𝓘(ℂ) (eisensteinSeries_SIF a k) :=
by
intro τ
suffices DifferentiableAt ℂ (↑ₕeisensteinSeries_SIF a k) τ.1
by
convert MDifferentiableAt.comp τ (DifferentiableAt.mdifferentiableAt this) τ.mdifferentiable_coe
exact funext fun z ↦ (comp_ofComplex (eisensteinSeries_SIF a k) z).symm
refine DifferentiableOn.differentiableAt ?_ (isOpen_upperHalfPlaneSet.mem_nhds τ.2)
exact
(eisensteinSeries_tendstoLocallyUniformlyOn hk a).differentiableOn
(Eventually.of_forall fun s ↦ DifferentiableOn.fun_sum fun _ _ ↦ eisSummand_extension_differentiableOn _ _)
isOpen_upperHalfPlaneSet
