Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_EisensteinSeries_EisensteinG.lean

definition module

Non-normalised level- Eisenstein series over a congruence class

For a natural number N, an integer k, a vector a \in (\mathbb{Z}/N\mathbb{Z})^2 (i.e. a : \mathrm{Fin}\,2 \to \mathbb{Z}/N\mathbb{Z}) and a point z of the upper half-plane, EisensteinSeries.eisensteinG N k a z is defined as the unconditional sum \sum_{\substack{v \in \mathbb{Z}^2 \\ v \equiv a \ (N)}} \mathrm{eisSummand}\,k\,v\,z, the index set being the subtype of those v : \mathrm{Fin}\,2 \to \mathbb{Z} whose componentwise reduction map \mathbb{Z} \to \mathbb{Z}/N\mathbb{Z} composed with v equals a, and the summand being Mathlib's Eisenstein summand, \mathrm{eisSummand}\,k\,v\,z = (v_0 z + v_1)^{-k} (a complex zpow). Thus, for k \ge 3, this is the classical non-normalised Eisenstein series G_k^{a}(z) = \sum (v_0 z + v_1)^{-k} of weight k for \Gamma(N) attached to the residue class a, the sum running over the entire congruence class and not only over its vectors with coprime entries.

Two points about the shape of the definition deserve note. First, the sum is a tsum, so the value is defined for every integer k and every N, and equals 0 by convention when the family fails to be summable; no convergence hypothesis is part of the definition. Second, when a = 0 the zero vector belongs to the index set, and it contributes 0^{-k}, which for k > 0 is 0 under the conventions for complex zpow, so that no term has to be removed by hand. The definition is made for arbitrary N : \mathbb{N}, the case N = 0 reading as the single vector v with \mathbb{Z}-coordinates prescribed by a under \mathbb{Z}/0\mathbb{Z} = \mathbb{Z}.

Relation to Mathlib

Mathlib's eisensteinSeries a k sums eisSummand only over the vectors of the class a with coprime entries (the gammaSet); EisensteinSeries.eisensteinG is the non-normalised variant, built from the same Mathlib summand eisSummand, summing over the whole congruence class modulo N.

Where it is used

This series is the project's concrete model of a weight-k level-\Gamma(N) Eisenstein series, with an explicit Fourier expansion at infinity, and is used in the modular-forms part of the development.

References

  1. F. Diamond and J. Shurman, A First Course in Modular Forms, Graduate Texts in Mathematics 228, Springer, 2005, §4.2
  2. T. Miyake, Modular Forms, Springer, 1989, §7.1
  3. E. Hecke, Theorie der Eisensteinschen Reihen höherer Stufe und ihre Anwendung auf Funktionentheorie und Arithmetik, Abh. Math. Sem. Univ. Hamburg 5 (1927), 199–224

References are suggested automatically and have not been individually verified.

English text generated automatically from the Lean source; the Lean statement is authoritative.

Source file: Definitions/Def_EisensteinSeries_EisensteinG.lean

Declarations

Source

import Mathlib

namespace EisensteinSeries

noncomputable def eisensteinG (N : ℕ) (k : ℤ) (a : Fin 2 → ZMod N) (z : UpperHalfPlane) : ℂ :=
  ∑' v : {v : Fin 2 → ℤ // ((↑) : ℤ → ZMod N) ∘ v = a}, eisSummand k v.1 z

end EisensteinSeries

Statements phrased using this module (3)