chore(NumberTheory/ModularForms): deprecation shims for moved level-one files#38991
Draft
CBirkbeck wants to merge 40 commits intoleanprover-community:masterfrom
Draft
chore(NumberTheory/ModularForms): deprecation shims for moved level-one files#38991CBirkbeck wants to merge 40 commits intoleanprover-community:masterfrom
CBirkbeck wants to merge 40 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`.
…level-one files Follow-up to leanprover-community#38806, which moved * `LevelOne.lean` → `LevelOne/Basic.lean` * `DimensionFormulas/LevelOne.lean` → `LevelOne/DimensionFormula.lean` without leaving deprecation stubs at the old paths (so that git rename-detection preserved file history). Now that the move has landed, this PR adds the deprecation shims back at the old paths so downstream users importing the old paths get a friendly `deprecated_module` warning pointing to the new location.
PR summary 6f6e20aa30Import changes for modified filesNo significant changes to the import graph Import changes for all files
|
github-actions
Bot
added
the
t-number-theory
mathlib-dependent-issues
Bot
added
the
blocked-by-other-PR
|
This PR/issue depends on:
|
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
1 participant
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.
Follow-up to #38806: re-adds deprecation shims at the old paths for files moved into
LevelOne/(so git rename detection in #38806 preserved blame).This PR was done with the help of Claude Code.