Eisenstein Series

Properties of the Eisenstein series E₄ and E₆, including their q-expansions.

Helper lemmas for dimension-one arguments

theorem exists_smul_eq_of_rank_one {M : Type u_1} [AddCommGroup M] [Module ℂ M] (hrank : Module.rank ℂ M = 1) {e : M} (he : e ≠ 0) (f : M) : ∃ (c : ℂ), f = c • e

In a rank-one module, every element is a scalar multiple of any nonzero element.

theorem smul_modularForm_eq_pointwise {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} {k : ℤ} {f g : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k} {c : ℂ} (h : f = c • g) (z : UpperHalfPlane) : f z = c * g z

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

Equations

• E₄ = E 4 E₄._proof_1

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

Equations

• E₆ = E 6 E₆._proof_1

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

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

E₆ is 1-periodic: E₆(z + 1) = E₆(z). This follows from E₆ being 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)

noncomputable def φ₀ (z : UpperHalfPlane) : ℂ

Equations

• φ₀ z = (E₂ z * E₄ z - E₆ z) ^ 2 / Δ z

noncomputable def φ₂' (z : UpperHalfPlane) : ℂ

Equations

• φ₂' z = E₄ z * (E₂ z * E₄ z - E₆ z) / Δ z

noncomputable def φ₄' (z : UpperHalfPlane) : ℂ

Equations

• φ₄' z = E₄ z ^ 2 / Δ z

noncomputable def φ₀'' (z : ℂ) : ℂ

Equations

• φ₀'' z = if hz : 0 < z.im then φ₀ { coe := z, coe_im_pos := hz } else 0

theorem φ₀''_def {z : ℂ} (hz : 0 < z.im) : φ₀'' z = φ₀ { coe := z, coe_im_pos := hz }

theorem φ₀''_coe_upperHalfPlane (z : UpperHalfPlane) : φ₀'' ↑z = φ₀ z

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 : (fun (m : ℕ) => (PowerSeries.coeff m) (UpperHalfPlane.qExpansion 1 ⇑E₆)) = fun (m : ℕ) => if m = 0 then 1 else -504 * ↑((ArithmeticFunction.sigma 5) m)

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

theorem E4E6_coeff_zero_eq_zero : (PowerSeries.coeff 0) (UpperHalfPlane.qExpansion 1 ((1 / 1728) • ⇑(((DirectSum.of (ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1))) 4) E₄ ^ 3 - (DirectSum.of (ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1))) 6) E₆ ^ 2) 12))) = 0

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

theorem neg_two_pi_I_pow_even_real (k : ℕ) (hk : Even k) : ((-2 * ↑Real.pi * Complex.I) ^ k).im = 0

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.

Boundedness of Eisenstein series

theorem E₄_isBoundedAtImInfty : UpperHalfPlane.IsBoundedAtImInfty E₄.toFun

E₄ is bounded at infinity (as a modular form).