diff --git a/Mathlib.lean b/Mathlib.lean index 3435a680bbbdec..be2866f8e408bd 100644 --- a/Mathlib.lean +++ b/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 diff --git a/Mathlib/NumberTheory/ModularForms/Basic.lean b/Mathlib/NumberTheory/ModularForms/Basic.lean index cfb4abba9ed314..8fe5991ef0b962 100644 --- a/Mathlib/NumberTheory/ModularForms/Basic.lean +++ b/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 diff --git a/Mathlib/NumberTheory/ModularForms/CuspFormSubmodule.lean b/Mathlib/NumberTheory/ModularForms/CuspFormSubmodule.lean index 5d38f28dbec919..dcd9a8cd6975d3 100644 --- a/Mathlib/NumberTheory/ModularForms/CuspFormSubmodule.lean +++ b/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 /-! diff --git a/Mathlib/NumberTheory/ModularForms/Discriminant.lean b/Mathlib/NumberTheory/ModularForms/Discriminant.lean index 582d40a8fefd1d..c283e2a4742ba4 100644 --- a/Mathlib/NumberTheory/ModularForms/Discriminant.lean +++ b/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 diff --git a/Mathlib/NumberTheory/ModularForms/EisensteinSeries/QExpansion.lean b/Mathlib/NumberTheory/ModularForms/EisensteinSeries/QExpansion.lean index 4c02bb54420f53..300dfb9bd5b2e7 100644 --- a/Mathlib/NumberTheory/ModularForms/EisensteinSeries/QExpansion.lean +++ b/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 diff --git a/Mathlib/NumberTheory/ModularForms/LevelOne.lean b/Mathlib/NumberTheory/ModularForms/LevelOne/Basic.lean similarity index 100% rename from Mathlib/NumberTheory/ModularForms/LevelOne.lean rename to Mathlib/NumberTheory/ModularForms/LevelOne/Basic.lean diff --git a/Mathlib/NumberTheory/ModularForms/DimensionFormulas/LevelOne.lean b/Mathlib/NumberTheory/ModularForms/LevelOne/DimensionFormula.lean similarity index 97% rename from Mathlib/NumberTheory/ModularForms/DimensionFormulas/LevelOne.lean rename to Mathlib/NumberTheory/ModularForms/LevelOne/DimensionFormula.lean index 0ddf7a000f7e55..dd37aa7f69b6b1 100644 --- a/Mathlib/NumberTheory/ModularForms/DimensionFormulas/LevelOne.lean +++ b/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 diff --git a/Mathlib/NumberTheory/ModularForms/LevelOne/GradedRing.lean b/Mathlib/NumberTheory/ModularForms/LevelOne/GradedRing.lean new file mode 100644 index 00000000000000..628e02aedd3126 --- /dev/null +++ b/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 diff --git a/Mathlib/NumberTheory/ModularForms/LevelOne/SturmBound.lean b/Mathlib/NumberTheory/ModularForms/LevelOne/SturmBound.lean new file mode 100644 index 00000000000000..a88a8675edf8e8 --- /dev/null +++ b/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 diff --git a/Mathlib/NumberTheory/ModularForms/NormTrace.lean b/Mathlib/NumberTheory/ModularForms/NormTrace.lean index 33837fc1a7c8e8..b1e0731fd3fc8d 100644 --- a/Mathlib/NumberTheory/ModularForms/NormTrace.lean +++ b/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 diff --git a/Mathlib/NumberTheory/ModularForms/QExpansion.lean b/Mathlib/NumberTheory/ModularForms/QExpansion.lean index 87d52a7155e495..c72a048c73539a 100644 --- a/Mathlib/NumberTheory/ModularForms/QExpansion.lean +++ b/Mathlib/NumberTheory/ModularForms/QExpansion.lean @@ -520,7 +520,7 @@ lemma qExpansion_one (h) : qExpansion h (1 : ℍ → ℂ) = 1 := by end UpperHalfPlane -namespace ModularFormClass +namespace ModularForm protected lemma cuspFunction_smul (hh : 0 < h) (hΓ : h ∈ Γ.strictPeriods) (a : ℂ) (f : F) [ModularFormClass F Γ k] : cuspFunction h (a • f) = a • cuspFunction h f := @@ -542,6 +542,12 @@ protected lemma cuspFunction_sub {G : Type*} [FunLike G ℍ ℂ] (hh : 0 < h) cuspFunction_sub (ModularFormClass.analyticAt_cuspFunction_zero f hh hΓ).continuousAt (ModularFormClass.analyticAt_cuspFunction_zero g hh hΓ).continuousAt +protected lemma cuspFunction_mul [Γ.HasDetPlusMinusOne] (hh : 0 < h) + (hΓ : h ∈ Γ.strictPeriods) {a b : ℤ} (f : ModularForm Γ a) (g : ModularForm Γ b) : + cuspFunction h (f.mul g) = cuspFunction h f * cuspFunction h g := + cuspFunction_mul (ModularFormClass.analyticAt_cuspFunction_zero f hh hΓ).continuousAt + (ModularFormClass.analyticAt_cuspFunction_zero g hh hΓ).continuousAt + protected lemma qExpansion_smul (hh : 0 < h) (hΓ : h ∈ Γ.strictPeriods) (a : ℂ) (f : F) [ModularFormClass F Γ k] : qExpansion h (a • f) = a • qExpansion h f := qExpansion_smul (ModularFormClass.analyticAt_cuspFunction_zero f hh hΓ) a @@ -562,16 +568,6 @@ protected lemma qExpansion_sub {G : Type*} [FunLike G ℍ ℂ] (hh : 0 < h) qExpansion_sub (ModularFormClass.analyticAt_cuspFunction_zero f hh hΓ) (ModularFormClass.analyticAt_cuspFunction_zero g hh hΓ) -end ModularFormClass - -namespace ModularForm - -protected lemma cuspFunction_mul [Γ.HasDetPlusMinusOne] (hh : 0 < h) - (hΓ : h ∈ Γ.strictPeriods) {a b : ℤ} (f : ModularForm Γ a) (g : ModularForm Γ b) : - cuspFunction h (f.mul g) = cuspFunction h f * cuspFunction h g := - cuspFunction_mul (ModularFormClass.analyticAt_cuspFunction_zero f hh hΓ).continuousAt - (ModularFormClass.analyticAt_cuspFunction_zero g hh hΓ).continuousAt - protected lemma qExpansion_mul [Γ.HasDetPlusMinusOne] (hh : 0 < h) (hΓ : h ∈ Γ.strictPeriods) {a b : ℤ} (f : ModularForm Γ a) (g : ModularForm Γ b) : qExpansion h (f.mul g) = qExpansion h f * qExpansion h g := @@ -587,12 +583,23 @@ protected lemma qExpansion_one [Γ.HasDetPlusMinusOne] : qExpansion h (1 : ModularForm Γ 0) = 1 := by simp [qExpansion_one] +protected lemma qExpansion_pow [Γ.HasDetPlusMinusOne] (hh : 0 < h) + (hΓ : h ∈ Γ.strictPeriods) (f : ModularForm Γ k) (n : ℕ) : + qExpansion h (f.pow n) = (qExpansion h f) ^ n := by + induction n with + | zero => + change qExpansion h (1 : ModularForm Γ 0) = _ + rw [pow_zero, ModularForm.qExpansion_one] + | succ n ih => + change qExpansion h ((f.pow n).mul f) = _ + rw [ModularForm.qExpansion_mul hh hΓ, ih, pow_succ] + /-- The qExpansion map as an additive group hom. to power series over `ℂ`. -/ def qExpansionAddHom (hh : 0 < h) (hΓ : h ∈ Γ.strictPeriods) (k : ℤ) : ModularForm Γ k →+ PowerSeries ℂ where toFun f := qExpansion h f map_zero' := qExpansion_zero h - map_add' f g := ModularFormClass.qExpansion_add hh hΓ f g + map_add' f g := ModularForm.qExpansion_add hh hΓ f g open scoped DirectSum in /-- The qExpansion map as a map from the graded ring of modular forms to power series over `ℂ`. -/ @@ -621,6 +628,34 @@ lemma qExpansion_of_pow [Γ.HasDetPlusMinusOne] (hh : 0 < h) end ModularForm +namespace ModularFormClass + +@[deprecated (since := "2026-05-05")] +protected alias cuspFunction_smul := ModularForm.cuspFunction_smul + +@[deprecated (since := "2026-05-05")] +protected alias cuspFunction_neg := ModularForm.cuspFunction_neg + +@[deprecated (since := "2026-05-05")] +protected alias cuspFunction_add := ModularForm.cuspFunction_add + +@[deprecated (since := "2026-05-05")] +protected alias cuspFunction_sub := ModularForm.cuspFunction_sub + +@[deprecated (since := "2026-05-05")] +protected alias qExpansion_smul := ModularForm.qExpansion_smul + +@[deprecated (since := "2026-05-05")] +protected alias qExpansion_neg := ModularForm.qExpansion_neg + +@[deprecated (since := "2026-05-05")] +protected alias qExpansion_add := ModularForm.qExpansion_add + +@[deprecated (since := "2026-05-05")] +protected alias qExpansion_sub := ModularForm.qExpansion_sub + +end ModularFormClass + end ring section uniqueness diff --git a/Mathlib/NumberTheory/ModularForms/SturmBound.lean b/Mathlib/NumberTheory/ModularForms/SturmBound.lean new file mode 100644 index 00000000000000..27647ed9c0e2da --- /dev/null +++ b/Mathlib/NumberTheory/ModularForms/SturmBound.lean @@ -0,0 +1,68 @@ +/- +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.SturmBound +public import Mathlib.NumberTheory.ModularForms.NormTrace + +/-! +# The Sturm bound for finite-index subgroups of `SL(2, ℤ)` + +For any finite-index subgroup `𝒢 ⊆ SL(2, ℤ)` and `f : ModularForm 𝒢 k`, if the q-expansion of +`f` at the cusp `∞` (with cusp width `𝒢.strictWidthInfty`) vanishes for the first +`⌊k * [SL(2, ℤ) : 𝒢] / 12⌋ + 1` coefficients, then `f = 0`. + +The proof lifts the level-one bound (`sturm_bound_levelOne`) via the norm map +`ModularForm.norm 𝒮ℒ : ModularForm 𝒢 k → ModularForm 𝒮ℒ (k * m)` (where `m = [SL(2,ℤ) : 𝒢]`): +the norm is identically zero precisely when `f` is, by `ModularForm.norm_eq_zero_iff`, and +sufficient vanishing of `f` at `∞` propagates to sufficient vanishing of `N(f)` at `∞`. + +## Main results + +* `ModularForm.sturm_bound_finiteIndex`: the Sturm bound for arbitrary finite-index `𝒢 ⊆ 𝒮ℒ`. +-/ + +@[expose] public noncomputable section + +open UpperHalfPlane ModularForm CuspForm MatrixGroups + +namespace ModularForm + +variable {𝒢 : Subgroup (GL (Fin 2) ℝ)} [𝒢.HasDetPlusMinusOne] [𝒢.IsFiniteRelIndex 𝒮ℒ] +variable {k : ℤ} (f : ModularForm 𝒢 k) + +/-- **Key bridge lemma.** The order of vanishing of `qExpansion 1 (norm 𝒮ℒ f)` at the cusp `∞` +is at least the order of vanishing of `qExpansion 𝒢.strictWidthInfty f` at the cusp `∞`. + +The proof writes `N(f) = ∏_q quotientFunc f q` and isolates the `𝒮ℒ_∞`-related factors (one +factor per element of `𝒮ℒ_∞ ⧸ 𝒢_∞`, i.e. `𝒢.strictWidthInfty` factors), whose product is +`1`-periodic and contributes order `(qExpansion 𝒢.strictWidthInfty f).order` in `q`. The +remaining factors are bounded at `∞` (since `f` is bounded at every cusp of `𝒢`), so they +contribute order `≥ 0`. -/ +private lemma qExpansion_norm_order_ge_qExpansion_order + [DiscreteTopology 𝒢.strictPeriods] : + (qExpansion 𝒢.strictWidthInfty f).order ≤ + (qExpansion 1 (ModularForm.norm 𝒮ℒ f)).order := by + sorry + +/-- **Sturm bound for finite-index subgroups of `SL(2, ℤ)`.** +If `f : ModularForm 𝒢 k` has zero coefficient on `q^i` in its q-expansion at the cusp `∞` +(at the natural period `𝒢.strictWidthInfty`) for every `i ≥ 0` with `12 * i ≤ k * [𝒮ℒ : 𝒢]`, +then `f = 0`. -/ +theorem sturm_bound_finiteIndex [DiscreteTopology 𝒢.strictPeriods] + (h : ∀ i : ℕ, 12 * (i : ℤ) ≤ k * Nat.card (𝒮ℒ ⧸ 𝒢.subgroupOf 𝒮ℒ) → + (qExpansion 𝒢.strictWidthInfty f).coeff i = 0) : f = 0 := by + rw [← coe_eq_zero_iff, ← ModularForm.norm_eq_zero_iff (ℋ := 𝒮ℒ)] + refine sturm_bound_levelOne (ModularForm.norm 𝒮ℒ f) fun i hi => ?_ + have h_le : ↑(i + 1) ≤ (qExpansion 𝒢.strictWidthInfty f).order := + PowerSeries.nat_le_order _ _ fun j hj => h j (by omega) + exact PowerSeries.coeff_of_lt_order _ <| + lt_of_lt_of_le (by exact_mod_cast Nat.lt_succ_self i) + (h_le.trans (qExpansion_norm_order_ge_qExpansion_order f)) + +end ModularForm + +end