Commit 2026-03-31 07:42 fdd294c6

feat(NumberTheory/ModularForms): modular discriminant as a cusp form (#36262)

Summary

This PR constructs the modular discriminant Δ(z) = η(z)^24 and proves it is a cusp form of weight 12 and level 1. The dominated convergence for infinite products is proved by reducing to the additive Tannery theorem via the formal expansion ∏ (1 + f i) = ∑ₛ ∏ᵢ∈ₛ f i.

New files

• Mathlib/Analysis/Normed/Ring/InfiniteProd.lean: Dominated convergence theorem for infinite products of the form ∏' k, (1 + f n k) in a complete normed commutative ring, proved via Tannery's theorem.
• Mathlib/NumberTheory/ModularForms/Discriminant.lean: The modular discriminant Δ, its q-expansion, non-vanishing, and slash-invariance under the generators of SL(2,ℤ).