feat(NumberTheory/ModularForms): Sturm bound for finite-index subgroups (WIP)

Mathlib.lean

@@ -5665,7 +5665,6 @@ public import Mathlib.NumberTheory.ModularForms.Cusps
 public import Mathlib.NumberTheory.ModularForms.DedekindEta
 public import Mathlib.NumberTheory.ModularForms.Delta
 public import Mathlib.NumberTheory.ModularForms.Derivative
-public import Mathlib.NumberTheory.ModularForms.DimensionFormulas.LevelOne
 public import Mathlib.NumberTheory.ModularForms.Discriminant
 public import Mathlib.NumberTheory.ModularForms.EisensteinSeries.Basic
 public import Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs
@@ -5683,13 +5682,17 @@ public import Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
 public import Mathlib.NumberTheory.ModularForms.JacobiTheta.Manifold
 public import Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable
 public import Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
-public import Mathlib.NumberTheory.ModularForms.LevelOne
+public import Mathlib.NumberTheory.ModularForms.LevelOne.Basic
+public import Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
+public import Mathlib.NumberTheory.ModularForms.LevelOne.GradedRing
+public import Mathlib.NumberTheory.ModularForms.LevelOne.SturmBound
 public import Mathlib.NumberTheory.ModularForms.NormTrace
 public import Mathlib.NumberTheory.ModularForms.Petersson
 public import Mathlib.NumberTheory.ModularForms.ProperlyDiscontinuous
 public import Mathlib.NumberTheory.ModularForms.QExpansion
 public import Mathlib.NumberTheory.ModularForms.SlashActions
 public import Mathlib.NumberTheory.ModularForms.SlashInvariantForms
+public import Mathlib.NumberTheory.ModularForms.SturmBound
 public import Mathlib.NumberTheory.MulChar.Basic
 public import Mathlib.NumberTheory.MulChar.Duality
 public import Mathlib.NumberTheory.MulChar.Lemmas

Mathlib/NumberTheory/ModularForms/Basic.lean

@@ -557,6 +557,7 @@ section GradedRing
 
 /-- Cast for modular forms, which is useful for avoiding `Heq`s. Optionally transports along
 an equality of subgroups. -/
+@[simps -fullyApplied coe]
 def mcast {a b : ℤ} {Γ Γ' : Subgroup (GL (Fin 2) ℝ)} (h : a = b) (f : ModularForm Γ a)
     (hΓ : Γ' = Γ := by rfl) : ModularForm Γ' b where
   toFun := (f : ℍ → ℂ)
@@ -571,6 +572,18 @@ theorem gradedMonoid_eq_of_cast {Γ : Subgroup (GL (Fin 2) ℝ)} {a b : GradedMo
   cases h
   exact congr_arg _ h2
 
+/-- The `n`-th power of a modular form, as a modular form of weight `n * k`. -/
+def pow {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.HasDetPlusMinusOne] {k : ℤ} (f : ModularForm Γ k)
+    (n : ℕ) : ModularForm Γ (n * k) :=
+  n.rec (mcast (by simp) (1 : ModularForm Γ 0)) (fun n g ↦ (g.mul f).mcast (by grind))
+
+@[simp]
+lemma coe_pow {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.HasDetPlusMinusOne] {k : ℤ}
+    (f : ModularForm Γ k) (n : ℕ) : ⇑(f.pow n) = (⇑f) ^ n := by
+  induction n with
+  | zero => simp [pow]
+  | succ n ih => simp_all only [pow, coe_mcast, coe_mul, pow_succ]
+
 instance (Γ : Subgroup (GL (Fin 2) ℝ)) [Γ.HasDetPlusMinusOne] :
     GradedMonoid.GOne (ModularForm Γ) where
   one := 1

Mathlib/NumberTheory/ModularForms/CuspFormSubmodule.lean

@@ -6,7 +6,7 @@ Authors: Chris Birkbeck
 module
 
 public import Mathlib.NumberTheory.ModularForms.QExpansion
-public import Mathlib.NumberTheory.ModularForms.LevelOne
+public import Mathlib.NumberTheory.ModularForms.LevelOne.Basic
 public import Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
 
 /-!

Mathlib/NumberTheory/ModularForms/Discriminant.lean

@@ -10,7 +10,7 @@ public import Mathlib.Analysis.Normed.Ring.InfiniteProd
 public import Mathlib.NumberTheory.ModularForms.DedekindEta
 public import Mathlib.NumberTheory.ModularForms.Basic
 public import Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform
-public import Mathlib.NumberTheory.ModularForms.LevelOne
+public import Mathlib.NumberTheory.ModularForms.LevelOne.Basic
 public import Mathlib.NumberTheory.ModularForms.QExpansion
 
 /-!
@@ -192,6 +192,33 @@ lemma exp_isBigO_discriminant : (fun τ ↦ Real.exp (-2 * π * τ.im)) =O[atImI
     grind [norm_one, norm_sub_rev]
   linarith [norm_nonneg (𝕢 1 τ), mul_le_mul_of_nonneg_left hprod_bound (norm_nonneg (𝕢 1 τ))]
 
+/-- The cusp function of the discriminant equals `q * ∏' n, (1 - q^(n+1))^24`
+on the open unit disc. -/
+private lemma discriminant_cuspFunction_eqOn : Set.EqOn (cuspFunction 1 Δ)
+    (fun q ↦ q * ∏' i, (1 - q ^ (i + 1)) ^ 24) (Metric.ball 0 1) := by
+  intro q hq
+  by_cases hq0 : q = 0
+  · simpa [hq0] using Periodic.cuspFunction_zero_of_zero_at_inf one_pos
+      discriminant_isZeroAtImInfty.zero_at_infty_comp_ofComplex
+  · have him := Periodic.im_invQParam_pos_of_norm_lt_one one_pos
+      (by simpa [dist_zero_right] using hq) hq0
+    simp [cuspFunction, Periodic.cuspFunction_eq_of_nonzero 1 _ hq0,
+      ofComplex_apply_of_im_pos him, discriminant_eq_q_prod ⟨_, him⟩,
+      Periodic.qParam_right_inv one_ne_zero hq0, eta_q]
+
+/-- The first q-expansion coefficient of the modular discriminant is 1. -/
+lemma discriminant_qExpansion_coeff_one : (qExpansion 1 Δ).coeff 1 = 1 := by
+  have hmem : (0 : ℂ) ∈ Metric.ball (0 : ℂ) 1 := Metric.mem_ball_self one_pos
+  calc (qExpansion 1 Δ).coeff 1
+      = derivWithin (cuspFunction 1 Δ) (Metric.ball 0 1) 0 := by
+        simp [qExpansion_coeff, ← derivWithin_of_isOpen Metric.isOpen_ball hmem]
+    _ = derivWithin (fun q ↦ q * ∏' i, (1 - q ^ (i + 1)) ^ 24) (Metric.ball 0 1) 0 :=
+        derivWithin_congr discriminant_cuspFunction_eqOn (discriminant_cuspFunction_eqOn hmem)
+    _ = 1 := by
+        simp [derivWithin_fun_mul differentiableWithinAt_id'
+          (differentiableOn_tprod_one_sub_pow_pow 24 _ hmem),
+          derivWithin_id' _ _ (Metric.isOpen_ball.uniqueDiffWithinAt hmem)]
+
 end
 
 end ModularForm

Mathlib/NumberTheory/ModularForms/EisensteinSeries/QExpansion.lean

@@ -10,7 +10,7 @@ public import Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
 public import Mathlib.NumberTheory.LSeries.Dirichlet
 public import Mathlib.NumberTheory.LSeries.HurwitzZetaValues
 public import Mathlib.NumberTheory.ModularForms.EisensteinSeries.Basic
-public import Mathlib.NumberTheory.ModularForms.LevelOne
+public import Mathlib.NumberTheory.ModularForms.LevelOne.Basic
 public import Mathlib.NumberTheory.TsumDivisorsAntidiagonal
 import Mathlib.Topology.EMetricSpace.Paracompact
 

Mathlib/NumberTheory/ModularForms/DimensionFormulas/LevelOne.lean → Mathlib/NumberTheory/ModularForms/LevelOne/DimensionFormula.lean

@@ -136,8 +136,8 @@ lemma ModularForm.rank_eq_one_add_rank_cuspForm {k : ℕ} (hk : 3 ≤ k) (hk2 :
     exact one_ne_zero <| hE.symm.trans <| (isCuspForm_iff_coeffZero_eq_zero _).mp h
   · refine (Submodule.Quotient.forall _).mpr fun f ↦ ⟨(qExpansion 1 f).coeff 0, ?_⟩
     rw [← Submodule.Quotient.mk_smul, Submodule.Quotient.eq, mem_cuspFormSubmodule_iff,
-      isCuspForm_iff_coeffZero_eq_zero, ModularForm.coe_sub, ModularFormClass.qExpansion_sub,
-      IsGLPos.coe_smul, ModularFormClass.qExpansion_smul, map_sub,
+      isCuspForm_iff_coeffZero_eq_zero, ModularForm.coe_sub, ModularForm.qExpansion_sub,
+      IsGLPos.coe_smul, ModularForm.qExpansion_smul, map_sub,
       PowerSeries.coeff_smul, E_qExpansion_coeff_zero hk hk2, smul_eq_mul, mul_one, sub_self]
     all_goals simp
 
@@ -187,12 +187,12 @@ private lemma weight_two_qExpansion_eq_zero (f : ModularForm 𝒮ℒ 2) : qExpan
       (Module.rank_eq_one_iff_finrank_eq_one.mp levelOne_weight_six_rank_one) _
   have hqc4 : c4 • qExpansion 1 (E₄ : ℍ → ℂ) = qExpansion 1 (f : ℍ → ℂ) ^ 2 := by
     rw [pow_two, ← ModularForm.qExpansion_mul one_pos one_mem_strictPeriods_SL f f,
-      ← ModularFormClass.qExpansion_smul one_pos one_mem_strictPeriods_SL c4 E₄,
+      ← ModularForm.qExpansion_smul one_pos one_mem_strictPeriods_SL c4 E₄,
       show (c4 • E₄ : ℍ → ℂ) = (f.mul f) from congrArg DFunLike.coe hc4]
   have hqc6 : c6 • qExpansion 1 E₆ = qExpansion 1 (f : ℍ → ℂ) ^ 3 := by
     rw [pow_succ, pow_two, ← ModularForm.qExpansion_mul one_pos one_mem_strictPeriods_SL f f,
       ← ModularForm.qExpansion_mul one_pos one_mem_strictPeriods_SL (f.mul f) f,
-      ← ModularFormClass.qExpansion_smul one_pos one_mem_strictPeriods_SL c6 E₆,
+      ← ModularForm.qExpansion_smul one_pos one_mem_strictPeriods_SL c6 E₆,
       show (c6 • E₆ : ℍ → ℂ) = (f.mul f).mul f from congrArg DFunLike.coe hc6]
   exact eq_zero_of_pow_eq_smul (E_qExpansion_coeff_zero _ ⟨2, rfl⟩)
     (E_qExpansion_coeff_zero _ ⟨3, rfl⟩) E₄_qExpansion_coeff_one E₆_qExpansion_coeff_one hqc4 hqc6

Mathlib/NumberTheory/ModularForms/LevelOne/GradedRing.lean

@@ -0,0 +1,97 @@
+/-
+Copyright (c) 2026 Chris Birkbeck. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Chris Birkbeck
+-/
+module
+
+public import Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
+
+/-!
+# The graded ring of level-1 modular forms
+
+This file collects structural results about the graded ring `⨁ k, ModularForm 𝒮ℒ k` of
+level-1 modular forms, beyond those that fall out of the dimension formula directly.
+
+## Main results
+
+* `ModularForm.discriminant_eq_E₄_cube_sub_E₆_sq`: the pointwise identity
+  `Δ = (E₄³ - E₆²) / 1728`.
+* `ModularForm.discriminant_eq_E₄_cube_sub_E₆_sq_graded`: the same identity in the graded
+  ring `⨁ k, ModularForm 𝒮ℒ k`.
+-/
+
+public noncomputable section
+
+open UpperHalfPlane ModularForm ModularFormClass MatrixGroups EisensteinSeries
+
+namespace ModularForm
+
+/-- The combination `E₄³ - E₆²` viewed as a level-1 modular form of weight 12. -/
+private noncomputable def E₄CubeSubE₆SqForm : ModularForm 𝒮ℒ 12 :=
+  ModularForm.mcast (by decide) (E₄.pow 3) - ModularForm.mcast (by decide) (E₆.pow 2)
+
+private lemma E₄CubeSubE₆SqForm_apply (z : ℍ) :
+    E₄CubeSubE₆SqForm z = E₄ z ^ 3 - E₆ z ^ 2 := by
+  simp only [E₄CubeSubE₆SqForm, coe_mcast, coe_pow, sub_apply, Pi.pow_apply]
+
+private lemma E₄CubeSubE₆SqForm_qExpansion_eq :
+    qExpansion 1 E₄CubeSubE₆SqForm = qExpansion 1 E₄ * qExpansion 1 E₄ * qExpansion 1 E₄ -
+      qExpansion 1 E₆ * qExpansion 1 E₆ := by
+  simp only [E₄CubeSubE₆SqForm, coe_sub, coe_mcast,
+    ModularForm.qExpansion_sub one_pos one_mem_strictPeriods_SL,
+    ModularForm.qExpansion_pow one_pos one_mem_strictPeriods_SL]
+  ring
+
+private lemma E₄CubeSubE₆SqForm_isCuspForm : IsCuspForm E₄CubeSubE₆SqForm := by
+  simp [isCuspForm_iff_coeffZero_eq_zero, E₄CubeSubE₆SqForm_qExpansion_eq,
+    PowerSeries.coeff_mul, -PowerSeries.coeff_zero_eq_constantCoeff,
+    E_qExpansion_coeff_zero _ ⟨2, rfl⟩, E_qExpansion_coeff_zero _ ⟨3, rfl⟩]
+
+private lemma E₄CubeSubE₆SqForm_qExpansion_coeff_one :
+    (qExpansion 1 E₄CubeSubE₆SqForm).coeff 1 = 1728 := by
+  rw [E₄CubeSubE₆SqForm_qExpansion_eq]
+  norm_num [PowerSeries.coeff_mul, Finset.Nat.antidiagonal_succ, E₄_qExpansion_coeff_one,
+    E₆_qExpansion_coeff_one, E_qExpansion_coeff_zero _ ⟨2, rfl⟩,
+    E_qExpansion_coeff_zero _ ⟨3, rfl⟩]
+
+/-- The modular discriminant equals `(E₄³ - E₆²) / 1728`. -/
+theorem discriminant_eq_E₄_cube_sub_E₆_sq (z : ℍ) :
+    discriminant z = (E₄ z ^ 3 - E₆ z ^ 2) / 1728 := by
+  obtain ⟨g, hg⟩ := E₄CubeSubE₆SqForm_isCuspForm
+  obtain ⟨c, hc⟩ := CuspForm.exists_smul_discriminant_of_weight_eq_twelve g
+  have hgE : (g : ℍ → ℂ) = E₄CubeSubE₆SqForm := congrArg DFunLike.coe hg
+  have hc_eq : c = 1728 := by
+    have hcΔ : (c • CuspForm.discriminant : ℍ → ℂ) = g := congrArg DFunLike.coe hc
+    have hgΔ := ModularForm.qExpansion_smul one_pos one_mem_strictPeriods_SL c
+      CuspForm.discriminant
+    rw [hcΔ, hgE] at hgΔ
+    simpa [PowerSeries.coeff_smul, discriminant_qExpansion_coeff_one,
+      E₄CubeSubE₆SqForm_qExpansion_coeff_one] using (congr_arg (·.coeff 1) hgΔ).symm
+  have h1728 : (1728 : ℂ) * discriminant z = E₄ z ^ 3 - E₆ z ^ 2 := by
+    rw [← hc_eq, show c * discriminant z = (c • CuspForm.discriminant) z from rfl, hc,
+      congr_fun hgE z, E₄CubeSubE₆SqForm_apply]
+  linear_combination h1728 / 1728
+
+/-- The modular discriminant equals `(E₄³ - E₆²) / 1728` in the graded ring
+`⨁ k, ModularForm 𝒮ℒ k`. -/
+theorem discriminant_eq_E₄_cube_sub_E₆_sq_graded :
+    DirectSum.of (ModularForm 𝒮ℒ) 12 CuspForm.discriminant =
+      (1 / 1728 : ℂ) • (.of (ModularForm 𝒮ℒ) 4 E₄ ^ 3 - .of (ModularForm 𝒮ℒ) 6 E₆ ^ 2) := by
+  have hE4 : DirectSum.of (ModularForm 𝒮ℒ) 4 E₄ ^ 3 = DirectSum.of (ModularForm 𝒮ℒ) 12
+      (ModularForm.mcast (by decide) ((E₄.mul E₄).mul E₄)) := by
+    rw [pow_succ (n := 2), pow_two, DirectSum.of_mul_of, DirectSum.of_mul_of]
+    rfl
+  have hE6 : DirectSum.of (ModularForm 𝒮ℒ) 6 E₆ ^ 2 =
+      DirectSum.of (ModularForm 𝒮ℒ) 12 (ModularForm.mcast (by decide) (E₆.mul E₆)) := by
+    rw [pow_two, DirectSum.of_mul_of]
+    rfl
+  rw [hE4, hE6, ← map_sub (DirectSum.of (ModularForm 𝒮ℒ) 12), ← DirectSum.of_smul]
+  congr 1
+  ext z
+  change ModularForm.discriminant z = (1 / 1728 : ℂ) * (E₄ z * E₄ z * E₄ z - E₆ z * E₆ z)
+  grind [discriminant_eq_E₄_cube_sub_E₆_sq z]
+
+end ModularForm
+
+end

Mathlib/NumberTheory/ModularForms/LevelOne/SturmBound.lean

@@ -0,0 +1,95 @@
+/-
+Copyright (c) 2026 Chris Birkbeck. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Chris Birkbeck
+-/
+module
+
+public import Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
+
+/-!
+# The Sturm bound for level-1 modular forms
+
+This file proves the *Sturm bound* for level-1 modular forms: a modular form of weight `k` for
+`SL(2, ℤ)` whose first `⌊k/12⌋ + 1` q-expansion coefficients all vanish must be identically zero.
+
+The proof iterates the isomorphism
+`CuspForm.discriminantEquiv : CuspForm 𝒮ℒ k ≃ₗ[ℂ] ModularForm 𝒮ℒ (k - 12)`
+(division by the modular discriminant `Δ`): a sufficiently-vanishing form is divisible by a power
+of `Δ`, landing eventually in negative weight where everything is zero.
+
+## Main results
+
+* `ModularForm.sturm_bound_levelOne`: the Sturm bound stated in the standard form: if every
+  coefficient of `q^i` in `qExpansion 1 f` with `12 * i ≤ k` is zero, then `f = 0`.
+-/
+
+@[expose] public noncomputable section
+
+open UpperHalfPlane ModularForm CuspForm MatrixGroups
+
+namespace ModularForm
+
+variable {k : ℤ} (f : ModularForm 𝒮ℒ k)
+
+private lemma qExpansion_eq_qExpansion_discriminant_mul
+    (hcusp : (qExpansion 1 f).coeff 0 = 0) :
+    qExpansion 1 f = qExpansion 1 discriminant *
+      qExpansion 1 (discriminantEquiv (toCuspForm f hcusp)) := by
+  have hfun : (f : ℍ → ℂ) = discriminant *
+      (CuspForm.discriminantEquiv (toCuspForm f hcusp) : ℍ → ℂ) := by
+    funext z
+    simp [CuspForm.discriminantEquiv, mul_div_cancel₀ _ (discriminant_ne_zero z)]
+  rw [hfun]
+  exact UpperHalfPlane.qExpansion_mul
+    (CuspForm.coe_discriminant ▸ ModularFormClass.analyticAt_cuspFunction_zero
+      (CuspForm.discriminant : CuspForm 𝒮ℒ 12) one_pos one_mem_strictPeriods_SL)
+    (ModularFormClass.analyticAt_cuspFunction_zero _ one_pos one_mem_strictPeriods_SL)
+
+private lemma orderOf_qExpansion_discriminant :
+    (qExpansion 1 ModularForm.discriminant).order = 1 := by
+  refine PowerSeries.order_eq_nat.mpr
+    ⟨ModularForm.discriminant_qExpansion_coeff_one ▸ one_ne_zero, fun i hi => ?_⟩
+  obtain rfl : i = 0 := by omega
+  have h0 := (isCuspForm_iff_coeffZero_eq_zero
+    ((CuspForm.discriminant : ModularForm 𝒮ℒ 12))).mp ⟨CuspForm.discriminant, rfl⟩
+  simpa using h0
+
+private lemma eq_zero_of_qExpansion_coeff_zero_lt (n : ℕ)
+    (hk : k < 12 * n) (hcoeff : ∀ i < n, (qExpansion 1 f).coeff i = 0) : f = 0 := by
+  induction n generalizing k f with
+  | zero =>
+    push_cast at hk
+    exact rank_zero_iff_forall_zero.mp
+      (ModularForm.levelOne_neg_weight_rank_zero (by omega)) f
+  | succ n ih =>
+    have h0 : (qExpansion 1 f).coeff 0 = 0 := hcoeff 0 (Nat.zero_lt_succ n)
+    set g := CuspForm.discriminantEquiv (toCuspForm f h0) with hg_def
+    have hg_order : ↑(n : ℕ) ≤ (qExpansion 1 g).order := by
+      refine (ENat.add_le_add_iff_left ENat.one_ne_top (k := 1)).mp ?_
+      rw [show (1 : ℕ∞) + ↑n = ((n + 1 : ℕ) : ℕ∞) by push_cast; ring,
+        ← orderOf_qExpansion_discriminant, ← PowerSeries.order_mul,
+        ← qExpansion_eq_qExpansion_discriminant_mul f h0]
+      exact PowerSeries.nat_le_order _ _ hcoeff
+    have hg_zero : g = 0 := ih g (by push_cast at hk; linarith) fun i hi =>
+      PowerSeries.coeff_of_lt_order _ (lt_of_lt_of_le (by exact_mod_cast hi) hg_order)
+    have hf' : toCuspForm f h0 = 0 :=
+      CuspForm.discriminantEquiv.injective (by simpa [← hg_def] using hg_zero)
+    ext z
+    simpa [toCuspForm_apply] using DFunLike.congr_fun hf' z
+
+/-- **Sturm bound for level-1 modular forms.** If a modular form `f` of weight `k` for `SL(2, ℤ)`
+has zero coefficient on `q^i` in its q-expansion for every `i ≥ 0` with `12 * i ≤ k`, then
+`f` is identically zero. -/
+theorem sturm_bound_levelOne
+    (h : ∀ i : ℕ, 12 * (i : ℤ) ≤ k → (qExpansion 1 f).coeff i = 0) : f = 0 := by
+  by_cases hk_neg : k < 0
+  · exact rank_zero_iff_forall_zero.mp (ModularForm.levelOne_neg_weight_rank_zero hk_neg) f
+  push Not at hk_neg
+  refine eq_zero_of_qExpansion_coeff_zero_lt f (k.toNat / 12 + 1) ?_ fun i hi => h i ?_
+  · omega
+  · omega
+
+end ModularForm
+
+end

Mathlib/NumberTheory/ModularForms/NormTrace.lean

@@ -5,7 +5,7 @@ Authors: David Loeffler
 -/
 module
 
-public import Mathlib.NumberTheory.ModularForms.LevelOne
+public import Mathlib.NumberTheory.ModularForms.LevelOne.Basic
 
 /-!
 # Norm and trace maps