E — Mathlib · SciLib

English

For hk ≥ 3, the level-1 normalised Eisenstein series E is defined by halving the level-1 Eisenstein series with zero Nebentypus, i.e. E_k = (1/2) eisensteinSeries_MF (mod_cast hk) 0.

Русский

Пусть hk ≥ 3. Нормализованный тождественный ряд Эйзенштейна уровня 1 задан как E_k = (1/2) EisensteinSeries_MF (mod_cast hk) 0.

LaTeX

$$$E_k = \frac{1}{2} \ eisensteinSeries\_MF(\mathrm{mod\_cast}(hk))\ 0 \in \mathcal{M}_{k}(\Gamma(1)).$$$

Lean4

/-- Normalised Eisenstein series of level 1 and weight `k`,
here they have been scaled by `1/2` since we sum over coprime pairs. -/
noncomputable def E {k : ℕ} (hk : 3 ≤ k) : ModularForm Γ(1) k :=
  (1 / 2 : ℂ) • eisensteinSeries_MF (mod_cast hk) 0

Похожие утверждения