English
Let N be a natural number and a be a function from Fin(2) to ZMod(N). For a given weight k and a point z in the upper half-plane, the Eisenstein series of weight k and level Γ(N) with congruence data a is defined by summing the local summands eisSummand(k, x, z) over a certain finite set gammaSet(N, 1, a).
Русский
Пусть N — натуральное число, а — отображение Fin(2) → ZMod(N). При заданном весе k и точке z в верхней полуплоскости Эйзенштейнова серия веса k и уровня Γ(N) с конгруэнтной величиной a задаётся как сумма локальных слагаемых eisSummand(k, x, z) по определённому конечному набору gammaSet(N, 1, a).
LaTeX
$$$E_{k,N,a}(z) = \sum_{x \in \gamma_N(1,a)} \mathrm{eisSummand}(k,x,z).$$$
Lean4
/-- An Eisenstein series of weight `k` and level `Γ(N)`, with congruence condition `a`. -/
def _root_.eisensteinSeries (k : ℤ) (z : ℍ) : ℂ :=
∑' x : gammaSet N 1 a, eisSummand k x z
