English
Let hk ≥ 3 and a: Fin 2 → ZMod N. Then there exists a modular form E_{k,N}(a) of weight k for the group Γ(N) whose underlying function is the Eisenstein series associated to a, with the standard slash-action and holomorphic on the upper half-plane, having the appropriate growth at cusps.
Русский
Пусть hk ≥ 3 и a: Fin 2 → ZMod N. Тогда существует конформная форма E_{k,N}(a) весом k для группы Γ(N), т. е. модульная форма Эйзенштейна, связанная с a, с обычным действием поSlash, голоморфна на верхней полуплоскости и имеет нужное поведение у мертвых пределов.
LaTeX
$$$E_{k,N}(a) \in \mathcal{M}_k(\Gamma(N)) \quad \land\quad E_{k,N}(a) = \text{EisensteinSeries}(a,k).$$$
Lean4
/-- This defines Eisenstein series as modular forms of weight `k`, level `Γ(N)` and congruence
condition given by `a : Fin 2 → ZMod N`. -/
def eisensteinSeries_MF {k : ℤ} {N : ℕ} [NeZero N] (hk : 3 ≤ k) (a : Fin 2 → ZMod N) : ModularForm Γ(N) k
where
toFun := eisensteinSeries_SIF a k
slash_action_eq' := (eisensteinSeries_SIF a k).slash_action_eq'
holo' := eisensteinSeries_SIF_MDifferentiable hk a
bdd_at_cusps' {c}
hc := by
rw [Subgroup.IsArithmetic.isCusp_iff_isCusp_SL2Z] at hc
rw [OnePoint.isBoundedAt_iff_forall_SL2Z hc]
exact fun γ hγ ↦ isBoundedAtImInfty_eisensteinSeries_SIF a hk γ
