The modular discriminant Δ

This file defines the modular discriminant Δ(z) = η(z) ^ 24, where η is the Dedekind eta function, and proves its key properties including invariance under the generators of SL(2, ℤ).

Main definitions

• ModularForm.discriminant: The modular discriminant function Δ(z) = η(z) ^ 24, which can also be expressed as q * ∏' (1 - q ^ (n + 1)) ^ 24 where q = e ^ (2πiz).

Main results

• ModularForm.discriminant_ne_zero: The discriminant is non-vanishing on the upper half-plane.
• ModularForm.discriminant_T_invariant: Invariance under the translation T : z ↦ z + 1.
• ModularForm.discriminant_S_invariant: Invariance under the inversion S : z ↦ -1 / z, showing Δ(-1 / z) = z ^ 12 · Δ(z).

References

• F. Diamond and J. Shurman, A First Course in Modular Forms, section 1.2

noncomputable def ModularForm.discriminant (z : UpperHalfPlane) : ℂ

The modular discriminant Δ(z) = η(z) ^ 24, where η is the Dedekind eta function.

Equations

• ModularForm.discriminant z = ModularForm.eta ↑z ^ 24

theorem ModularForm.discriminant_eq_q_prod (z : UpperHalfPlane) : discriminant z = Function.Periodic.qParam 1 ↑z * ∏' (n : ℕ), (1 - eta_q n ↑z) ^ 24

The discriminant expressed as a q-expansion: Δ(z) = q * ∏' (1 - q ^ (n + 1)) ^ 24.

theorem ModularForm.discriminant_ne_zero (z : UpperHalfPlane) : discriminant z ≠ 0

The modular discriminant is non-vanishing on the upper half-plane.

theorem ModularForm.discriminant_T_invariant : SlashAction.map 12 ModularGroup.T discriminant = discriminant

The discriminant is invariant under T : z ↦ z + 1, i.e., Δ(z + 1) = Δ(z).

theorem ModularForm.eta_comp_eq_csqrt_I_inv : Set.EqOn (eta ∘ fun (x : ℂ) => -1 / x) (Complex.I.sqrt⁻¹ • (Complex.sqrt * eta)) UpperHalfPlane.upperHalfPlaneSet

The transformation formula for η under S : z ↦ -1 / z: we have η(-1 / z) = (√I)⁻¹ · √z · η(z) on the upper half-plane.

theorem ModularForm.discriminant_S_invariant : SlashAction.map 12 ModularGroup.S discriminant = discriminant

The discriminant satisfies the modular transformation for S : z ↦ -1 / z: we have Δ(-1 / z) = z ^ 12 · Δ(z).

theorem ModularForm.discriminant_bounded_factor : Filter.Tendsto (fun (x : UpperHalfPlane) => ∏' (n : ℕ), (1 - eta_q n ↑x) ^ 24) UpperHalfPlane.atImInfty (nhds 1)

theorem ModularForm.discriminant_isZeroAtImInfty : UpperHalfPlane.IsZeroAtImInfty discriminant

noncomputable def ModularForm.discriminantCuspForm : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range 12

The modular discriminant Δ as a cusp form of weight 12 and level 1.

Equations

• One or more equations did not get rendered due to their size.