Fermat's Last Theorem in Lean 4

← all definition modules

Definitions/Def_EisensteinSeries_WeierstrassZeta.lean

definition module

Weierstrass zeta function and weight-one Eisenstein functions

For \tau in the upper half-plane write \Lambda_\tau = \mathbb{Z}\tau + \mathbb{Z} and, for v \in \mathbb{Z}^2 (indexed as a function Fin 2 → ℤ), \omega_v = v_0\tau + v_1. The first definition, EisensteinSeries.weierstrassZeta τ z, is the Weierstrass zeta function of \Lambda_\tau, Z(\tau,z) = \frac{1}{z} + \sum_{v \in \mathbb{Z}^2} \Bigl(\frac{1}{z-\omega_v} + \frac{1}{\omega_v} + \frac{z}{\omega_v^2}\Bigr), where the summand at v = 0 is replaced by 0 and the sum is taken as an unconditional sum over the whole index set \mathbb{Z}^2 rather than over an exhaustion by finite subsets. Division is Lean's total division on \mathbb{C}, with 1/0 = 0; consequently the expression also returns a value at z = 0 and at the other points of \Lambda_\tau, where the classical function has its poles.

The second definition, EisensteinSeries.eisensteinG1 N v τ, attaches to a level N \in \mathbb{N} and a vector v = (v_0, v_1) \in \mathbb{Z}^2 the function of \tau g_1^{v}(\tau) = \frac{1}{N}\Bigl(Z\bigl(\tau, \tfrac{v_0\tau + v_1}{N}\bigr) - \frac{v_0\bigl(\tau G_2(\tau) - 2\pi i\bigr) + v_1 G_2(\tau)}{N}\Bigr), where G_2 is the weight-two Eisenstein series. The subtracted term is the linear combination of the quasi-periods \eta_1(\tau) = \tau G_2(\tau) - 2\pi i and \eta_2(\tau) = G_2(\tau) of Z with coefficients v_0, v_1, divided by N; it is written out directly in terms of G_2 rather than defined as a difference Z(\tau, z + \omega) - Z(\tau, z). Both definitions are plain formulas: no holomorphy, summability or modular transformation property is part of the data.

Relation to Mathlib

The weight-two Eisenstein series G_2 used in eisensteinG1 is Mathlib's EisensteinSeries.G2, and both definitions are placed in the same EisensteinSeries namespace; the Weierstrass zeta function of the lattice \mathbb{Z}\tau + \mathbb{Z} and the weight-one functions g_1^{v} are the project's own.

Where it is used

These formulas are the starting point for the development of weight-one Eisenstein series for \Gamma(N) in the modules that import this one, where the quasi-periodicity of Z is used to establish the dependence of g_1^{v} on v modulo N and its weight-one transformation behaviour under SL_2(\mathbb{Z}).

References

  1. F. Diamond and J. Shurman, A First Course in Modular Forms, Graduate Texts in Mathematics 228, Springer, 2005, §4.8
  2. S. Lang, Elliptic Functions, 2nd edition, Graduate Texts in Mathematics 112, Springer, 1987, Chapter 18
  3. J. H. Silverman, Advanced Topics in the Arithmetic of Elliptic Curves, Graduate Texts in Mathematics 151, Springer, 1994, Chapter I, §§5–6

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_WeierstrassZeta.lean

Declarations

Source

import Mathlib

namespace EisensteinSeries

noncomputable def weierstrassZeta (τ : UpperHalfPlane) (z : ℂ) : ℂ :=
  1 / z + ∑' v : Fin 2 → ℤ, if v = 0 then 0 else
    (1 / (z - ((v 0 : ℂ) * τ + v 1)) + 1 / ((v 0 : ℂ) * τ + v 1) + z / ((v 0 : ℂ) * τ + v 1) ^ 2)

noncomputable def eisensteinG1 (N : ℕ) (v : Fin 2 → ℤ) (τ : UpperHalfPlane) : ℂ :=
  1 / (N : ℂ) *
    (weierstrassZeta τ (((v 0 : ℂ) * τ + v 1) / N) -
      ((v 0 : ℂ) * ((τ : ℂ) * G2 τ - 2 * Real.pi * Complex.I) + (v 1 : ℂ) * G2 τ) / N)

end EisensteinSeries

Statements phrased using this module (4)