The modular discriminant Δ

Mathlib's ModularForm.discriminant provides the modular discriminant together with its fundamental properties: non-vanishing (ModularForm.discriminant_ne_zero), invariance under the generators of SL(2, ℤ), decay at i∞, and the associated cusp form CuspForm.discriminant of weight 12 for 𝒮ℒ. This file introduces the notation Δ for it and provides the complements used in this project:

• Δ_eq_cexp_prod, DiscriminantProductFormula: the q-product for Δ written with explicit complex exponentials, indexed by ℕ and ℕ+ respectively.
• Δ_periodic, Δ_S_transform: pointwise transformation laws under the generators.
• Δ_imag_axis_pos: Δ is real and positive on the positive imaginary axis.

The Modular Discriminant Δ

Properties of the modular discriminant Δ.

def termΔ : Lean.ParserDescr

Δ is mathlib's modular discriminant ModularForm.discriminant.

Equations

• termΔ = Lean.ParserDescr.node `termΔ 1024 (Lean.ParserDescr.symbol "Δ")

theorem MultipliableEtaProductExpansion_pnat (z : UpperHalfPlane) : Multipliable fun (n : ℕ+) => 1 - Complex.exp (2 * ↑Real.pi * Complex.I * ↑↑n * ↑z)

theorem Δ_eq_cexp_prod (z : UpperHalfPlane) : Δ z = Complex.exp (2 * ↑Real.pi * Complex.I * ↑z) * ∏' (n : ℕ), (1 - Complex.exp (2 * ↑Real.pi * Complex.I * (↑n + 1) * ↑z)) ^ 24

The discriminant as a q-product with explicit complex exponentials.

theorem DiscriminantProductFormula (z : UpperHalfPlane) : Δ z = Complex.exp (2 * ↑Real.pi * Complex.I * ↑z) * ∏' (n : ℕ+), (1 - Complex.exp (2 * ↑Real.pi * Complex.I * ↑↑n * ↑z)) ^ 24

theorem Δ_periodic (z : UpperHalfPlane) : Δ (1 +ᵥ z) = Δ z

Δ is 1-periodic: Δ (z + 1) = Δ z.

theorem Δ_S_transform (z : UpperHalfPlane) : Δ (ModularGroup.S • z) = ↑z ^ 12 * Δ z

Δ transforms under S as Δ (-1 / z) = z ^ 12 * Δ z.

theorem Δ_boundedfactor : Filter.Tendsto (fun (x : UpperHalfPlane) => ∏' (n : ℕ), (1 - Complex.exp (2 * ↑Real.pi * Complex.I * (↑n + 1) * ↑x)) ^ 24) UpperHalfPlane.atImInfty (nhds 1)

theorem Δ_imag_axis_pos : ResToImagAxis.Pos Δ

Δ is real and positive on the positive imaginary axis.