feat(NumberTheory/ModularForms): Sturm bound for level-1 modular forms#38993
Draft
CBirkbeck wants to merge 47 commits intoleanprover-community:masterfrom
Draft
feat(NumberTheory/ModularForms): Sturm bound for level-1 modular forms#38993CBirkbeck wants to merge 47 commits intoleanprover-community:masterfrom
CBirkbeck wants to merge 47 commits intoleanprover-community:masterfrom
Conversation
…e dimension formula Adds `CuspFormSubmodule.lean` providing the cusp form submodule of modular forms together with API, and `DimensionFormulas/LevelOne.lean` proving the classical dimension formula for spaces of level one modular forms. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Targeted fixes from PR leanprover-community#37789 review: - `cuspFormSubmodule` and `equivCuspFormSubmodule`: make `Γ`/`k` explicit - `isCuspForm_iff`: shorter proof - `ofMulDiscriminant`: simplify cusp-form coeff zero argument - `divDiscriminant.holo'`: golf by inlining the differentiability subgoals - `rank_eq_one_add_rank_cuspForm`: take `hk : 3 ≤ k` over `ℕ` - `discriminant_eq_E4_cube_sub_E6_sq`: restate as `Δ = (E₄³ - E₆²)/1728`, drop inline proof comments, fold redundant `have`s - `exists_smul_eq_of_rank_one`: use `finrank_eq_one_iff_of_nonzero'` from mathlib - Move `one_mem_strictPeriods_SL` to `LevelOne.lean` so the haveI workaround in `EisensteinSeries.E_qExpansion_coeff` can be dropped Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
…ula proofs - `discriminant_eq_E4_cube_sub_E6_sq`: hoist `hmcast` (used 3x) above its use, drop redundant calc step `_ = (CuspForm.toModularFormₗ g) z := rfl` - `weight_two_eq_zero_of_not_cuspForm`: drop `hc0`, fold the c4/c6 substitutions directly into `heq4`/`heq6` rather than via separate `hc4_eq`/`hc6_eq` + `rw`, replace the by_contra finale with `pow_eq_zero_iff`/`mul_eq_zero` Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Add public `noncomputable abbrev`s `ModularForm.E₄ : ModularForm 𝒮ℒ 4` and `ModularForm.E₆ : ModularForm 𝒮ℒ 6` for the normalised level 1 Eisenstein series of weights 4 and 6. Use them throughout `DimensionFormulas/LevelOne.lean` to drop the awkward `E (show 3 ≤ 4 by norm_num)` and `set E4 := …` patterns. The `abbrev` (rather than `def` or notation) is required so all uses share a single underlying proof of `3 ≤ 4` / `3 ≤ 6`, which lets simp lemmas about their q-expansions match consistently. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
…oor_sub_div` Adds the lemma `⌊k / a⌋₊ = 1 + ⌊(k - a) / a⌋₊` for `0 < a ≤ k` over a linear ordered field, generalising the local `floor_lem1` helper that was buried in `DimensionFormulas/LevelOne.lean`. Inline the helper at its single use site in `dimension_level_one`. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
…lpers up to DedekindEta
Adds three q-coordinate lemmas to `DedekindEta.lean`:
- `multipliable_one_sub_pow {q : ℂ} (hq : ‖q‖ < 1)`: pointwise multipliability
- `multipliableLocallyUniformlyOn_one_sub_pow`: local uniform convergence on the
open unit disc
- `differentiableOn_tprod_one_sub_pow_pow (k : ℕ)`: differentiability of the
k-th power of the product on the open unit disc
These cover the case `q = 0` (the cusp at infinity), which the existing eta-side
lemmas (`multipliableLocallyUniformlyOn_eta` etc., stated on `ℍₒ`) cannot.
In `Discriminant.lean`, deletes the three private helpers
`multipliable_one_sub_pow`, `tendstoLocallyUniformlyOn_eta_prod`,
`differentiableWithinAt_eta_prod_pow`, and rewrites `discriminant_cuspFunction_eqOn`
and `discriminant_qExpansion_coeff_one` to work on the full open unit disc
`Metric.ball 0 1` (instead of the arbitrary `Metric.ball 0 (1/2)`) and to call
the new helpers from `DedekindEta.lean`.
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
…-coord base Rather than having parallel q-coord and z-coord proofs of the same convergence facts about the eta product, derive the z-coord versions from the q-coord ones by composing with `Periodic.qParam 1 : ℍₒ → Metric.ball 0 1`. - `multipliableLocallyUniformlyOn_eta` is now derived from `multipliableLocallyUniformlyOn_one_sub_pow` via `TendstoLocallyUniformlyOn.comp`, shrinking the proof from ~14 lines to ~7. - `differentiableAt_eta_tprod` now derives from `differentiableOn_tprod_one_sub_pow` by chain rule (instead of going through the eta-side multipliable lemma). - `summable_eta_q` switched to `norm_qParam_lt_one` (which the q-coord material already uses) for consistency. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
…lyOn_eta` `hasProdLocallyUniformlyOn_iff_tendstoLocallyUniformlyOn` is `Iff.rfl`, so the two `rw` calls in the previous proof are unnecessary — a type ascription on the underlying `HasProdLocallyUniformlyOn` is enough to invoke `TendstoLocallyUniformlyOn.comp` via dot notation. Collapse the proof to a 6-line term-mode expression. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Extracts helper lemmas to shorten the two main proofs: - `tendsto_valueAtInfty`: a modular form whose `valueAtInfty` is `c` tends to `c` along `atImInfty`. Used in `E4_cube_sub_E6_sq_form_isCuspForm`. - `E4_cube_sub_E6_sq_form` (def): the explicit `ModularForm 𝒮ℒ 12` whose pointwise value is `E₄³ - E₆²`, with companion lemmas `_apply`, `_isCuspForm`, `_qExpansion_coeff_one`. The main theorem `discriminant_eq_E4_cube_sub_E6_sq` is now ~15 lines instead of ~70. - `coeffZero_eq_zero_of_pow_eq_smul`: the algebraic core of the weight-2 vanishing argument as a pure power-series fact (no modular forms). `weight_two_eq_zero_of_not_cuspForm` becomes a thin wrapper that transports the modular-form identities into the power-series form, shrinking from ~50 lines to ~25. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
…ter decomposition - `discriminant_eq_E4_cube_sub_E6_sq`: move `hgΔ` back inside the local `hc_eq` block (it's only used there), inline `hgF`, and use `simpa` for the final step. - `E4_cube_sub_E6_sq_form_qExpansion_coeff_one`: minor simplification collapsing the chained `mcast`/`hmcast` rewrites. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Wraps several lines in the dimension-formula proofs to fit within mathlib's 100-character line length limit. No semantic changes. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
…sion lemmas `E₄` and `E₆` are `noncomputable abbrev`s, so they reduce automatically and the explicit `show E₄ = E (...) from rfl` step in `E₄_qExpansion_coeff_one` and `E₆_qExpansion_coeff_one` was unnecessary. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Adds `CuspForm.toModularForm` and a `Coe (CuspForm Γ k) (ModularForm Γ k)` instance so cusp forms can be viewed as modular forms automatically. Refactors `CuspForm.toModularFormₗ` to delegate to this plain function and updates call sites. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
…ubmodule Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Restores ModularForm.discriminant_eq_E4_cube_sub_E6_sq, ported from earlier work (commit 8d90310) and updated to current master's API: - discriminantCuspForm → CuspForm.discriminant - cuspForm_twelve_smul_discriminant → CuspForm.exists_smul_discriminant_of_weight_eq_twelve - qExpansion_sub/qExpansion_smul → ModularFormClass.qExpansion_sub/qExpansion_smul - The `IsCuspForm` proof uses an algebraic q-expansion split rather than the no-longer-available tendsto_valueAtInfty. Adds supporting lemmas in Discriminant.lean: - discriminant_cuspFunction_eqOn (private) - differentiableWithinAt_eta_prod_pow (private; shorter than original since differentiableOn_tprod_one_sub_pow_pow is now in mathlib) - discriminant_qExpansion_coeff_one Also drops merge-induced duplicates of master lemmas (summable_eta_q, multipliableLocallyUniformlyOn_eta, differentiableOn_tprod_one_sub_pow, differentiableOn_tprod_one_sub_pow_pow, one_mem_strictPeriods_SL) and removes two unused/duplicating helpers (floor_div_eq_one_add_floor_sub_div, which is too specific for a top-level file and unused, and ModularForm.ofSubgroupEq, which duplicates mcast).
Applies findings from /simplify code review: - Extract the duplicated `qExpansion_sub` rewrite chain into a shared `E₄CubeSubE₆SqForm_qExpansion_eq` helper. Both `_isCuspForm` and `_qExpansion_coeff_one` now reduce to a one-line `rw` of this helper (~16 lines saved). - `linear_combination (1 / 1728 : ℂ) * h1728` → `linear_combination h1728 / 1728`. - Rename `E4_cube_sub_E6_sq_form` → `E₄CubeSubE₆SqForm` (camelCase + subscripts per mathlib def naming convention) and `discriminant_eq_E4_cube_sub_E6_sq` → `discriminant_eq_E₄_cube_sub_E₆_sq`. - Use `ball 0 1` instead of `ball 0 (1/2)` in `discriminant_cuspFunction_eqOn` and `discriminant_qExpansion_coeff_one` (the actual constraint is `‖q‖ < 1`), which lets `differentiableOn_tprod_one_sub_pow_pow` apply directly and removes the now-unnecessary `differentiableWithinAt_eta_prod_pow` helper.
Drops `(... : ℍ → ℂ)` type ascriptions where the surrounding term already forces the coercion (`qExpansion 1 E₄`, `cuspFunction 1 Δ`, `qExpansion 1 E₄CubeSubE₆SqForm`, etc.). Also reflows the affected declarations to fit the 100-character line limit.
…²) / 1728
Adds `ModularForm.discriminant_eq_E₄_cube_sub_E₆_sq_graded`, the analogue of
`discriminant_eq_E₄_cube_sub_E₆_sq` in the graded ring `⨁ k, ModularForm 𝒮ℒ k`:
DirectSum.of (ModularForm 𝒮ℒ) 12 (CuspForm.discriminant : ModularForm 𝒮ℒ 12) =
(1 / 1728 : ℂ) • (DirectSum.of (ModularForm 𝒮ℒ) 4 E₄ ^ 3 -
DirectSum.of (ModularForm 𝒮ℒ) 6 E₆ ^ 2)
The proof reduces to the pointwise identity via `DirectSum.of_mul_of`, `congr 1`,
and `ext`, then closes by `discriminant_eq_E₄_cube_sub_E₆_sq` and `ring`.
In `discriminant_eq_E₄_cube_sub_E₆_sq_graded`, replace `(by norm_num)` proofs of `4 + 4 + 4 = 12` and `6 + 6 = 12` with `(by decide)` (kernel reduction).
Adds `@[simp]` lemmas `ModularForm.mcast_apply` and `CuspForm.mcast_apply` saying `mcast h f hΓ z = f z` (true by `rfl`). These let `simp` automatically unfold `mcast` in pointwise reasoning, and are useful API for any future proofs that mix `ModularForm.mcast`/`CuspForm.mcast` with `simp`-based function-level rewriting.
The simp lemmas were unused — `change` in `discriminant_eq_E₄_cube_sub_E₆_sq_graded` goes through defeq directly, and the `simp only`-based alternatives I tried didn't close the goal. Removing per "no unused API" guideline; can be re-added later when there's a proof that benefits. This reverts commit 8de2aff.
…adedRing.lean Splits the `Δ = (E₄³ - E₆²) / 1728` results out of `DimensionFormulas/LevelOne.lean` into a new file `DimensionFormulas/GradedRing.lean`. This new file is intended to collect structural results about the graded ring `⨁ k, ModularForm 𝒮ℒ k` of level-1 modular forms (e.g. that `E₄, E₆` generate the full graded ring, to come). Moved declarations: - `E₄CubeSubE₆SqForm` (private) - `E₄CubeSubE₆SqForm_apply` (private) - `E₄CubeSubE₆SqForm_qExpansion_eq` (private) - `E₄CubeSubE₆SqForm_isCuspForm` (private) - `E₄CubeSubE₆SqForm_qExpansion_coeff_one` (private) - `discriminant_eq_E₄_cube_sub_E₆_sq` - `discriminant_eq_E₄_cube_sub_E₆_sq_graded`
…s/ root Move `DimensionFormulas/GradedRing.lean` → `GradedRing.lean`. The graded-ring results aren't specifically about dimension formulas, so they belong at the top of the `ModularForms/` directory.
…y#38806 - Discriminant.lean: convert single `simp` for `discriminant_qExpansion_coeff_one` to a 3-step `calc` proof for robustness. - Basic.lean: add `ModularForm.pow` (with `coe_pow` simp lemma). - QExpansion.lean: add `ModularForm.qExpansion_pow`. - GradedRing.lean: use `pow` and `qExpansion_pow` in the `E₄³ - E₆²` def. - QExpansion.lean: move `cuspFunction_smul/neg/add/sub` and `qExpansion_smul/neg/add/sub` from `ModularFormClass` to `ModularForm` namespace, per the convention that lemmas about `Foo` go in the `Foo` namespace even when their input is class-generic. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
`LevelOne.lean` and `DimensionFormulas/LevelOne.lean` existed on master, so moving their content into `LevelOne/Basic.lean` and `LevelOne/DimensionFormula.lean` must leave deprecation shims at the old paths — otherwise `Mathlib.lean`'s existing imports of those paths point at missing files and CI fails with `bad import`. Each shim is a `module -- shake: keep-all` stub that `public import`s the new location plus `deprecated_module ... (since := "2026-05-05")`. Note: `GradedRing.lean` was added in this PR (no master version), so no shim is needed for it.
…riminant-identity
…istory Per loefflerd's followup on this PR: > If the old file doesn't vanish entirely, but gets reduced to a one-line > deprecation stub, then Git treats the newly-relocated file as if it were > freshly created. So `LevelOne.lean` and `DimensionFormulas/LevelOne.lean` are simply removed here (the move into `LevelOne/Basic.lean` and `LevelOne/DimensionFormula.lean` preserves git history). A separate follow-up PR will reintroduce deprecation shims at those old paths for downstream users. `Mathlib.lean` updated via `lake exe mk_all`.
A modular form `f` of weight `k` for `SL(2, ℤ)` whose first `⌊k/12⌋ + 1` q-expansion coefficients all vanish must be identically zero. The proof iterates `CuspForm.discriminantEquiv` (cusp forms ≃ modular forms of weight `k - 12` via division by `Δ`): a sufficiently-vanishing form is divisible by a power of `Δ`, eventually landing in negative weight where `ModularFormClass.levelOne_neg_weight_eq_zero` finishes. * `ModularForm.eq_zero_of_qExpansion_coeff_zero_lt` (private auxiliary form) * `ModularForm.sturm_bound_levelOne` (the main theorem)
Cleanup pass via /cleanup: * `analyticAt_cuspFunction_discriminant`: term-mode via `▸`. * `qExpansion_eq_qExpansion_discriminant_mul`: drop `hfun_z` intermediate, inline `h1`. * `eq_zero_of_qExpansion_coeff_zero_lt`: inline `hqE`/`hf_order`/`hgcoeff`/`hz`, collapse the ℕ∞ arithmetic, term-mode `hf'`. * `sturm_bound_levelOne`: drop two unused `hkn` haves — `omega` handles `Int.toNat` directly given the nonneg hypothesis. 128 → 113 lines.
…interval_cases` /simplify pass: * Extract `eq_zero_of_neg_weight` private helper to dedupe the `coe_eq_zero_iff` + `levelOne_neg_weight_eq_zero` pattern (used 2×). * `WithTop.add_le_add_iff_left` → `ENat.add_le_add_iff_left` (more idiomatic for the ℕ∞ type). * `interval_cases i` (with `i < 1`) → `obtain rfl : i = 0 := by omega` (lighter machinery for a single value). * Inline single-use `hcusp` in `orderOf_qExpansion_discriminant`.
github-actions
Bot
added
the
t-number-theory
PR summary 6f6e20aa30
|
| Files | Import difference |
|---|---|
Mathlib.NumberTheory.ModularForms.DimensionFormulas.LevelOne |
-3091 |
Mathlib.NumberTheory.ModularForms.LevelOne |
-2781 |
Mathlib.NumberTheory.ModularForms.LevelOne.Basic |
2781 |
Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula |
3091 |
Mathlib.NumberTheory.ModularForms.LevelOne.GradedRing (new file) Mathlib.NumberTheory.ModularForms.LevelOne.SturmBound (new file) |
3092 |
Declarations diff
+ E₄CubeSubE₆SqForm
+ E₄CubeSubE₆SqForm_apply
+ E₄CubeSubE₆SqForm_isCuspForm
+ E₄CubeSubE₆SqForm_qExpansion_coeff_one
+ E₄CubeSubE₆SqForm_qExpansion_eq
+ coe_pow
+ cuspFunction_add
+ cuspFunction_neg
+ cuspFunction_smul
+ cuspFunction_sub
+ discriminant_cuspFunction_eqOn
+ discriminant_eq_E₄_cube_sub_E₆_sq
+ discriminant_eq_E₄_cube_sub_E₆_sq_graded
+ discriminant_qExpansion_coeff_one
+ eq_zero_of_qExpansion_coeff_zero_lt
+ orderOf_qExpansion_discriminant
+ pow
+ qExpansion_add
+ qExpansion_eq_qExpansion_discriminant_mul
+ qExpansion_neg
+ qExpansion_pow
+ qExpansion_smul
+ qExpansion_sub
+ sturm_bound_levelOne
You can run this locally as follows
## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>
## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.
No changes to strong technical debt.
No changes to weak technical debt.
note: file Mathlib/NumberTheory/ModularForms/DimensionFormulas/LevelOne.lean` was renamed to `Mathlib/NumberTheory/ModularForms/LevelOne/DimensionFormula.lean without a module deprecation
Please create a follow-up pull request adding one. Thanks!
note: file Mathlib/NumberTheory/ModularForms/LevelOne.lean` was renamed to `Mathlib/NumberTheory/ModularForms/LevelOne/Basic.lean without a module deprecation
Please create a follow-up pull request adding one. Thanks!
github-actions
Bot
added
the
file-removed
Both `analyticAt_cuspFunction_discriminant` and `eq_zero_of_neg_weight` were thin wrappers around existing mathlib API: * `analyticAt_cuspFunction_discriminant` was a one-use specialization of `ModularFormClass.analyticAt_cuspFunction_zero` for `Δ`. Inlined. * `eq_zero_of_neg_weight` (`f = 0` for negative weight) follows from `ModularForm.levelOne_neg_weight_rank_zero` plus `rank_zero_iff_forall_zero`.
mathlib-dependent-issues
Bot
added
the
blocked-by-other-PR
|
This PR/issue depends on:
|
Per-declaration deep golf: * `qExpansion_eq_qExpansion_discriminant_mul`: drop `set g`/`have hsymm` scaffolding; use `funext fun z ↦ simp [CuspForm.discriminantEquiv, mul_div_cancel₀ _ (discriminant_ne_zero z)]` directly. (17 → 11 lines) * `orderOf_qExpansion_discriminant`: collapse first bullet via `▸`, replace `rwa [show … from coe_discriminant]` with `simpa using h0` (since `coe_discriminant` is `@[simp]`). (11 → 8 lines) * `eq_zero_of_qExpansion_coeff_zero_lt`: restructure the ℕ∞-arithmetic block — invert the chain so `ENat.add_le_add_iff_left` runs once at the start, then a single `rw` sequence reaches `nat_le_order`. (29 → 26 lines) 107 → 95 lines.
Two minor cleanups suggested in review:
* `variable {k : ℤ}` after `namespace ModularForm`, removing the per-lemma
`{k : ℤ}` binders.
* `eq_zero_of_qExpansion_coeff_zero_lt` now takes `n` as a parameter and
uses `induction n generalizing k f` instead of stating `∀ n, ...` and
manually `intro`-ing each case.
`variable (f : ModularForm 𝒮ℒ k)` after the namespace; per-lemma `f` binders dropped from `qExpansion_eq_qExpansion_discriminant_mul`, `eq_zero_of_qExpansion_coeff_zero_lt`, and `sturm_bound_levelOne`. The `f`-first argument order at the `eq_zero_of_qExpansion_coeff_zero_lt` call site is updated accordingly.
Avoids a `simp` nested inside a `rw [show ... from ...]`. The statement of `hfun` is also self-documenting now.
Contributor
|
Standard question: what's the extent of LLM involvement here? (I haven't seen humans being their PR description with |
Collaborator
Author
|
Oh its all done by Claude. I havent added the LLM tag yet since its still a draft and I havent finished going through it myself yet. |
grunweg
added
the
LLM-generated
Contributor
|
Thanks! Let me add the label now; I'll leave the PR description to you. |
Collaborator
Author
|
Just to check, should I be adding this label even while they are still in draft? if so I'll do a couple of others ones I have, Edit: I guess the answer is clearly yes, so I'll do that from now on. |
1 task
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
The Sturm bound for level 1: a modular form
f : ModularForm 𝒮ℒ kwhose first⌊k/12⌋ + 1q-expansion coefficients vanish is identically zero. The proof iteratesCuspForm.discriminantEquivuntil the weight goes negative.This PR was done with the help of Claude Code.