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.delta: 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.delta_ne_zero: The discriminant is non-vanishing on the upper half-plane.
• ModularForm.delta_T_invariant: Invariance under the translation T : z ↦ z + 1.
• ModularForm.delta_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.delta (z : UpperHalfPlane) : ℂ

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

Equations

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

theorem ModularForm.delta_eq_q_prod (z : UpperHalfPlane) : delta 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.delta_ne_zero (z : UpperHalfPlane) : delta z ≠ 0

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

theorem ModularForm.delta_T_invariant : SlashAction.map 12 ModularGroup.T delta = delta

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.delta_S_invariant : SlashAction.map 12 ModularGroup.S delta = delta

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