noncomputable def ComplexLattice.eisensteinSeries (L : ComplexLattice) (k : ℕ) : ℂ

The weight-k Eisenstein series of a lattice L, defined as G_k(L) = ∑' l∈L \{0}, 1 / l^k. Packaged as L.G k from ComplexLattice.

@[simp]

theorem ComplexLattice.eisensteinSeries_def (L : ComplexLattice) (k : ℕ) : L.eisensteinSeries k = ∑' (l : ↥(PeriodPair.lattice L)), (↑l ^ k)⁻¹

Definitional unfolding of L.eisensteinSeries k as the sum ∑' l : L.lattice, (l^k)⁻¹.

theorem ComplexLattice.hasSum_eisensteinSeries (L : ComplexLattice) {k : ℕ} (hk : 2 < k) : HasSum (fun (l : ↥(PeriodPair.lattice L)) => (↑l ^ k)⁻¹) (L.eisensteinSeries k)

For k > 2, the family l ↦ (l^k)⁻¹ indexed by the lattice L is summable, with sum equal to the weight-k Eisenstein series L.eisensteinSeries k.

theorem ComplexLattice.summable_eisensteinSeries (L : ComplexLattice) {k : ℕ} (hk : 2 < k) : Summable fun (l : ↥(PeriodPair.lattice L)) => (↑l ^ k)⁻¹

For k > 2, the family l ↦ (l^k)⁻¹ is summable.

theorem ComplexLattice.summable_norm_eisensteinSeries (L : ComplexLattice) {k : ℕ} (hk : 2 < k) : Summable fun (l : ↥(PeriodPair.lattice L)) => ‖(↑l ^ k)⁻¹‖

For k > 2, the family l ↦ (l^k)⁻¹ is absolutely summable (norm summable).

theorem ComplexLattice.g₂_eq (L : ComplexLattice) : PeriodPair.g₂ L = 60 * L.eisensteinSeries 4

The classical modular invariant g₂(L) equals 60 times the weight-4 Eisenstein series G_4(L).

theorem ComplexLattice.g₃_eq (L : ComplexLattice) : PeriodPair.g₃ L = 140 * L.eisensteinSeries 6

The classical modular invariant g₃(L) equals 140 times the weight-6 Eisenstein series G_6(L).

def ComplexLattice.ofUpperHalfPlane (τ : UpperHalfPlane) : ComplexLattice

The lattice ℤ + ℤτ ⊂ ℂ associated to a point τ in the upper half-plane.

noncomputable def g₂Function (τ : UpperHalfPlane) : ℂ

The function τ ↦ g₂(ℤ + ℤτ) on the upper half-plane.

noncomputable def g₃Function (τ : UpperHalfPlane) : ℂ

The function τ ↦ g₃(ℤ + ℤτ) on the upper half-plane.

noncomputable def discriminantFunction (τ : UpperHalfPlane) : ℂ

The modular discriminant function Δ(τ) = g₂(τ)^3 - 27 g₃(τ)^2 on the upper half-plane.

noncomputable def jFunction (τ : UpperHalfPlane) : ℂ

The modular j-function j(τ) = 1728 g₂(τ)^3 / Δ(τ) on the upper half-plane.

def UpperHalfPlane.addOne (τ : UpperHalfPlane) : UpperHalfPlane

The translation τ ↦ τ + 1 on the upper half-plane (it preserves the upper half-plane because the imaginary part is unchanged).

noncomputable def UpperHalfPlane.negInv (τ : UpperHalfPlane) : UpperHalfPlane

The inversion τ ↦ -1/τ on the upper half-plane (preserves the upper half-plane because Im(-1/τ) = Im τ / |τ|² > 0).

theorem lattice_ofUpperHalfPlane_eq_addOne (τ : UpperHalfPlane) : PeriodPair.lattice (ComplexLattice.ofUpperHalfPlane τ) = PeriodPair.lattice (ComplexLattice.ofUpperHalfPlane τ.addOne)

The lattices ℤ + ℤτ and ℤ + ℤ(τ + 1) coincide as subsets of ℂ, since τ + 1 is obtained from τ by an SL₂(ℤ)-translation.

theorem isHomothetic_ofUpperHalfPlane_negInv (τ : UpperHalfPlane) : (ComplexLattice.ofUpperHalfPlane τ).IsHomothetic (ComplexLattice.ofUpperHalfPlane τ.negInv)

The lattices ℤ + ℤτ and ℤ + ℤ(-1/τ) are homothetic via the scalar τ⁻¹.

theorem ComplexLattice.jInvariantLattice_eq_of_lattice_eq {L L' : ComplexLattice} (h : PeriodPair.lattice L = PeriodPair.lattice L') : L.jInvariantLattice = L'.jInvariantLattice

The j-invariant of a complex lattice depends only on the underlying set of lattice points: if L.lattice = L'.lattice, then j(L) = j(L').

theorem ComplexLattice.jInvariantLattice_eq_of_isHomothetic {L L' : ComplexLattice} (h : L.IsHomothetic L') : L'.jInvariantLattice = L.jInvariantLattice

The j-invariant is homothety-invariant: if L and L' are homothetic lattices, then they have the same j-invariant.

theorem jFunction_add_one (τ : UpperHalfPlane) : jFunction τ.addOne = jFunction τ

The j-function is invariant under translation by 1: j(τ + 1) = j(τ). This is one of the modular-invariance properties of j in Theorem 15.8 of Sutherland's Elliptic Curves.

theorem jFunction_neg_inv (τ : UpperHalfPlane) : jFunction τ.negInv = jFunction τ

The j-function is invariant under τ ↦ -1/τ: j(-1/τ) = j(τ). This is the second modular-invariance property of j in Theorem 15.8 of Sutherland's Elliptic Curves.

noncomputable def g₂Ext (z : ℂ) : ℂ

Extension of g₂Function to all of ℂ, set to 0 outside the upper half-plane.

noncomputable def g₃Ext (z : ℂ) : ℂ

Extension of g₃Function to all of ℂ, set to 0 outside the upper half-plane.

theorem g₂Ext_differentiableOn : DifferentiableOn ℂ g₂Ext {z : ℂ | 0 < z.im}

The extended g₂Ext is holomorphic on the upper half-plane {z : Im z > 0}.

theorem g₃Ext_differentiableOn : DifferentiableOn ℂ g₃Ext {z : ℂ | 0 < z.im}

The extended g₃Ext is holomorphic on the upper half-plane {z : Im z > 0}.

theorem ComplexLattice.discriminantLattice_ne_zero' (L : ComplexLattice) : L.discriminantLattice ≠ 0

The lattice discriminant Δ(L) = g₂(L)³ - 27 g₃(L)² never vanishes for a complex lattice L.

theorem jFunction_ext_eq (z : ℂ) (hz : 0 < z.im) : (if h : 0 < z.im then jFunction { coe := z, coe_im_pos := h } else 0) = 1728 * g₂Ext z ^ 3 / (g₂Ext z ^ 3 - 27 * g₃Ext z ^ 2)

Definitional equality expressing the extended j-function on the upper half-plane in terms of the extended g₂ and g₃: j(z) = 1728 g₂(z)^3 / (g₂(z)^3 - 27 g₃(z)^2).

theorem discriminant_ext_ne_zero (z : ℂ) (hz : 0 < z.im) : g₂Ext z ^ 3 - 27 * g₃Ext z ^ 2 ≠ 0

The lattice discriminant g₂(z)^3 - 27 g₃(z)^2 (as an extended function) is nonzero on the upper half-plane.

theorem jFunction_holomorphic : DifferentiableOn ℂ (fun (z : ℂ) => if h : 0 < z.im then jFunction { coe := z, coe_im_pos := h } else 0) {z : ℂ | 0 < z.im}

The j-function is holomorphic on the upper half-plane. This is the holomorphy assertion of Theorem 15.8 of Sutherland's Elliptic Curves ("The j-function is holomorphic on ℍ, and satisfies j(-1/τ) = j(τ) and j(τ + 1) = j(τ)").