The Eisenstein series E₄ and E₆

This file defines the normalised level-one Eisenstein series E k (as ModularForm Γ(1) k, with constant term 1; mathlib's ModularForm.E is typed over 𝒮ℒ, the two coincide as functions on ℍ), its specialisations E₄ and E₆, and collects the properties of E₂, E₄ and E₆ needed by the project (the quotients φ₀, φ₂', φ₄' by Δ live in SpherePacking.MagicFunction.a.Phi):

• E₄_periodic, E₆_periodic, E₄_S_transform, E₆_S_transform: pointwise transformation laws under the generators of SL(2, ℤ).
• E4_q_exp, E4_q_exp_zero, E6_q_exp_zero: explicit q-expansion coefficients (240 · σ₃ for E₄).
• Ek_ne_zero, E4_ne_zero, E6_ne_zero: non-vanishing, via mathlib's EisensteinSeries.E_ne_zero.
• E_even_imag_axis_real, E₂_imag_axis_real, E₄_imag_axis_real, E₆_imag_axis_real: realness on the positive imaginary axis.

Boundedness of E₂ at i∞ is now mathlib's EisensteinSeries.isBoundedAtImInfty_E2.

Definitions and transformation laws

noncomputable def E (k : ℤ) (hk : 3 ≤ k) : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k

The normalised Eisenstein series of weight k and level one, with constant term 1. The scaling by 1/2 matches the normalisation, since the sum is taken over coprime pairs.

Equations

• E k hk = (1 / 2) • ModularForm.eisensteinSeriesMF hk 0

noncomputable def E₄ : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) 4

The normalised Eisenstein series of weight 4 and level one, with constant term 1.

Equations

• E₄ = E 4 E₄._proof_1

noncomputable def E₆ : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) 6

The normalised Eisenstein series of weight 6 and level one, with constant term 1.

Equations

• E₆ = E 6 E₆._proof_1

theorem E₄_periodic (z : UpperHalfPlane) : E₄ (1 +ᵥ z) = E₄ z

E₄ is 1-periodic: E₄(z + 1) = E₄(z), as a modular form for Γ(1).

theorem E₆_periodic (z : UpperHalfPlane) : E₆ (1 +ᵥ z) = E₆ z

E₆ is 1-periodic: E₆(z + 1) = E₆(z), as a modular form for Γ(1).

theorem E₄_S_transform (z : UpperHalfPlane) : E₄ (ModularGroup.S • z) = ↑z ^ 4 * E₄ z

E₄ transforms under S as: E₄(-1/z) = z⁴ · E₄(z)

theorem E₆_S_transform (z : UpperHalfPlane) : E₆ (ModularGroup.S • z) = ↑z ^ 6 * E₆ z

E₆ transforms under S as: E₆(-1/z) = z⁶ · E₆(z)

q-expansion coefficients and non-vanishing

theorem E4_q_exp : (fun (m : ℕ) => (PowerSeries.coeff m) (UpperHalfPlane.qExpansion 1 ⇑E₄)) = fun (m : ℕ) => if m = 0 then 1 else 240 * ↑((ArithmeticFunction.sigma 3) m)

theorem E4_q_exp_zero : (PowerSeries.coeff 0) (UpperHalfPlane.qExpansion 1 ⇑E₄) = 1

theorem E6_q_exp_zero : (PowerSeries.coeff 0) (UpperHalfPlane.qExpansion 1 ⇑E₆) = 1

theorem Ek_ne_zero (k : ℕ) (hk : 3 ≤ ↑k) (hk2 : Even k) : E (↑k) hk ≠ 0

theorem E4_ne_zero : E₄ ≠ 0

theorem E6_ne_zero : E₆ ≠ 0

Realness on the imaginary axis

theorem exp_imag_axis_arg (t : ℝ) (ht : 0 < t) (n : ℕ+) : 2 * ↑Real.pi * Complex.I * ↑{ coe := Complex.I * ↑t, coe_im_pos := ⋯ } * ↑↑n = ↑(-(2 * Real.pi * ↑↑n * t))

On imaginary axis z = I*t, the q-expansion exponent 2πi·n·z reduces to -(2πnt). This is useful for reusing the same algebraic simplification across E₂, E₄, E₆.

theorem E_even_imag_axis_real (k : ℕ) (hk : 3 ≤ ↑k) (hk2 : Even k) : ResToImagAxis.Real (E (↑k) hk).toFun

E_k(it) is real for all t > 0 when k is even and k ≥ 4. This is the generalized theorem from which E₄_imag_axis_real and E₆_imag_axis_real follow.

theorem E₄_imag_axis_real : ResToImagAxis.Real E₄.toFun

E₄(it) is real for all t > 0.

theorem E₆_imag_axis_real : ResToImagAxis.Real E₆.toFun

E₆(it) is real for all t > 0.

theorem E₂_imag_axis_real : ResToImagAxis.Real E₂

E₂(it) is real for all t > 0.