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.tendsto_atImInfty_tprod_one_sub_eta_q_pow : Filter.Tendsto (fun (x : UpperHalfPlane) => ∏' (n : ℕ), (1 - eta_q n ↑x) ^ 24) UpperHalfPlane.atImInfty (nhds 1)

@[deprecated ModularForm.tendsto_atImInfty_tprod_one_sub_eta_q_pow (since := "2026-04-30")]

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

Alias of ModularForm.tendsto_atImInfty_tprod_one_sub_eta_q_pow.

theorem ModularForm.discriminant_isZeroAtImInfty : UpperHalfPlane.IsZeroAtImInfty discriminant

theorem ModularForm.exp_isBigO_discriminant : (fun (τ : UpperHalfPlane) => Real.exp (-2 * Real.pi * τ.im)) =O[UpperHalfPlane.atImInfty] discriminant

theorem ModularForm.discriminant_cuspFunction_eqOn : Set.EqOn (UpperHalfPlane.cuspFunction 1 discriminant) (fun (q : ℂ) => q * ∏' (i : ℕ), (1 - q ^ (i + 1)) ^ 24) (Metric.ball 0 1)

The cusp function of the discriminant equals q * ∏' n, (1 - q^(n+1))^24 on the open unit disc.

theorem ModularForm.discriminant_qExpansion_coeff_one : (PowerSeries.coeff 1) (UpperHalfPlane.qExpansion 1 discriminant) = 1

The first q-expansion coefficient of the modular discriminant is 1.

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

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

Equations

• CuspForm.discriminant = { toFun := ModularForm.discriminant, slash_action_eq' := ⋯, holo' := CuspForm.discriminant._proof_3, zero_at_cusps' := ⋯ }

@[simp]

theorem CuspForm.coe_discriminant : ⇑discriminant = ModularForm.discriminant

theorem CuspForm.exp_decay_isBigO_discriminant {k : ℤ} (f : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k) : ⇑f =O[UpperHalfPlane.atImInfty] ModularForm.discriminant

Any cusp form for 𝒮ℒ is O(Δ) at the cusp i∞.

@[deprecated CuspForm.discriminant (since := "2026-04-30")]

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

Alias of CuspForm.discriminant.

---

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

Equations

• ModularForm.discriminantCuspForm = CuspForm.discriminant