English
There is a SlashInvariantForm associated to an Eisenstein series, built from the function eisensteinSeries a k and equipped with a compatibility condition with the Gamma(N)–SL(2) action. This object encodes the SL-invariance data in a convenient form.
Русский
Сопоставлена SlashInvariantForm-цепочка, связанная с рядом Эйзенштейна, построенная на функции eisensteinSeries a k и оборудованная совместимостью с действием Γ(N)–SL(2). Этот объект кодирует данные инвариантности относительно SL.
LaTeX
$$$\text{eisensteinSeries\_SIF}(a,k) := \{ \text{toFun} = \mathrm{eisensteinSeries}(a,k), \ \text{slash\_action\_eq'} \text{(A,hA)} \}.$$$
Lean4
/-- The SlashInvariantForm defined by an Eisenstein series of weight `k : ℤ`, level `Γ(N)`,
and congruence condition given by `a : Fin 2 → ZMod N`. -/
def eisensteinSeries_SIF (k : ℤ) : SlashInvariantForm (Gamma N) k
where
toFun := eisensteinSeries a k
slash_action_eq' A
hA := by
obtain ⟨A, (hA : A ∈ Γ(N)), rfl⟩ := hA
simp [SpecialLinearGroup.mapGL, ← SL_slash, eisensteinSeries_slash_apply, Gamma_mem'.mp hA]
