feat(NumberTheory/ModularForms): dimension formula for level one modular forms (#37979)

Proves the classical dimension formula for the space of modular forms of level 1 (`SL(2, ℤ)`) and even weight `k`:

$$\dim M_k(\mathrm{SL}(2,\mathbb{Z})) = \lfloor k/12 \rfloor  \text{ if } k \equiv 2 \pmod{12}, \qquad\lfloor k/12 \rfloor + 1  \text{ otherwise.}$$

The work was done as part of the Sphere packing project.

Author: CBirkbeck

Mathlib.lean

@@ -5655,6 +5655,7 @@ 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

Mathlib/NumberTheory/ModularForms/Basic.lean

@@ -227,6 +227,15 @@ theorem zero_apply (z : ℍ) : (0 : ModularForm Γ k) z = 0 :=
     (f : ℍ → ℂ) = 0 ↔ f = 0 := by
   rw [← coe_zero, DFunLike.coe_fn_eq]
 
+/-- If `-1 ∈ Γ` and `k` is odd, then every modular form of weight `k` for `Γ` is zero. -/
+lemma eq_zero_of_neg_one_mem [Γ.HasDetOne] (h_neg_one : -1 ∈ Γ) (hk : Odd k)
+    (f : ModularForm Γ k) : f = 0 := by
+  ext z
+  have hf := slash_action_eqn'' f h_neg_one z
+  rw [neg_smul, one_smul, denom_neg, denom_one, hk.neg_one_zpow] at hf
+  have h2 : (2 : ℂ) * f z = 0 := by linear_combination hf
+  exact (mul_eq_zero.mp h2).resolve_left (by norm_num)
+
 section
 -- scalar multiplication by real types (no assumption on `Γ`)
 
@@ -520,19 +529,40 @@ instance (priority := 99) [FunLike F ℍ ℂ] [CuspFormClass F Γ k] : ModularFo
   holo := CuspFormClass.holo
   bdd_at_cusps f _ hc g hg := (CuspFormClass.zero_at_cusps f hc g hg).boundedAtFilter
 
+/-- Multiplying a `CuspForm` by a `ModularForm` gives a `CuspForm` (the cusp condition is
+preserved since a function tending to zero times a bounded function tends to zero). -/
+@[simps! -fullyApplied coe]
+def mulModularForm [Γ.HasDetPlusMinusOne] {k₁ k₂ : ℤ} (f : CuspForm Γ k₁) (g : ModularForm Γ k₂) :
+    CuspForm Γ (k₁ + k₂) where
+  toSlashInvariantForm := f.1.mul g.1
+  holo' := f.holo'.mul g.holo'
+  zero_at_cusps' hc γ hγ := by
+    simpa [mul_slash] using
+      ((f.zero_at_cusps' hc γ hγ).mul_boundedAtFilter (g.bdd_at_cusps' hc γ hγ)).smul _
+
+/-- Cast for cusp forms, which is useful for avoiding `Heq`s. Optionally transports along
+an equality of subgroups. -/
+def mcast {a b : ℤ} {Γ Γ' : Subgroup (GL (Fin 2) ℝ)} (h : a = b) (f : CuspForm Γ a)
+    (hΓ : Γ' = Γ := by rfl) : CuspForm Γ' b where
+  toFun := (f : ℍ → ℂ)
+  slash_action_eq' A hA := h ▸ f.slash_action_eq' A (hΓ ▸ hA)
+  holo' := f.holo'
+  zero_at_cusps' hc := h ▸ f.zero_at_cusps' (hΓ ▸ hc)
+
 end CuspForm
 
 namespace ModularForm
 
 section GradedRing
 
-/-- Cast for modular forms, which is useful for avoiding `Heq`s. -/
-def mcast {a b : ℤ} {Γ : Subgroup (GL (Fin 2) ℝ)} (h : a = b) (f : ModularForm Γ a) :
-    ModularForm Γ b where
+/-- Cast for modular forms, which is useful for avoiding `Heq`s. Optionally transports along
+an equality of subgroups. -/
+def mcast {a b : ℤ} {Γ Γ' : Subgroup (GL (Fin 2) ℝ)} (h : a = b) (f : ModularForm Γ a)
+    (hΓ : Γ' = Γ := by rfl) : ModularForm Γ' b where
   toFun := (f : ℍ → ℂ)
-  slash_action_eq' A := h ▸ f.slash_action_eq' A
+  slash_action_eq' A hA := h ▸ f.slash_action_eq' A (hΓ ▸ hA)
   holo' := f.holo'
-  bdd_at_cusps' A := h ▸ f.bdd_at_cusps' A
+  bdd_at_cusps' hc := h ▸ f.bdd_at_cusps' (hΓ ▸ hc)
 
 @[ext (iff := false)]
 theorem gradedMonoid_eq_of_cast {Γ : Subgroup (GL (Fin 2) ℝ)} {a b : GradedMonoid (ModularForm Γ)}

Mathlib/NumberTheory/ModularForms/DedekindEta.lean

@@ -62,25 +62,51 @@ noncomputable def eta (z : ℂ) := 𝕢 24 z * ∏' n, (1 - eta_q n z)
 /-- Notation for the Dedekind eta function. -/
 scoped[ModularForm] notation "η" => eta
 
+/-- For `‖q‖ < 1`, the infinite product `∏ (1 - q^(n+1))` is multipliable. -/
+lemma multipliable_one_sub_pow {q : ℂ} (hq : ‖q‖ < 1) :
+    Multipliable fun n : ℕ ↦ 1 - q ^ (n + 1) := by
+  apply multipliable_one_add_of_summable (f := fun n ↦ -q ^ (n + 1))
+  simpa using (summable_nat_add_iff 1).mpr (summable_geometric_of_lt_one (norm_nonneg _) hq)
+
+/-- The infinite product `∏ (1 - q^(n+1))` converges locally uniformly on the open unit disc,
+with limit `q ↦ ∏' n, (1 - q^(n+1))`. -/
+lemma multipliableLocallyUniformlyOn_one_sub_pow :
+    MultipliableLocallyUniformlyOn (fun n q ↦ 1 - q ^ (n + 1)) (Metric.ball (0 : ℂ) 1) := by
+  use fun q ↦ ∏' n, (1 - q ^ (n + 1))
+  simp_rw [sub_eq_add_neg]
+  apply hasProdLocallyUniformlyOn_of_forall_compact Metric.isOpen_ball
+  intro K hK hcK
+  rcases K.eq_empty_or_nonempty with hN | hN
+  · simpa [hasProdUniformlyOn_iff_tendstoUniformlyOn, hN] using tendstoUniformlyOn_empty
+  · obtain ⟨q₀, hq₀, _, HB⟩ := hcK.exists_sSup_image_eq_and_ge hN
+      (show ContinuousOn (fun q : ℂ ↦ ‖q‖) K by fun_prop)
+    refine ((summable_nat_add_iff 1).mpr (summable_geometric_of_lt_one (norm_nonneg _)
+      (by simpa [Metric.mem_ball, dist_zero_right] using hK hq₀))).hasProdUniformlyOn_nat_one_add
+      hcK (.of_forall fun n x hx ↦ ?_) (fun _ ↦ by fun_prop)
+    simpa using pow_le_pow_left₀ (norm_nonneg _) (HB x hx) (n + 1)
+
+/-- The infinite product `q ↦ ∏' n, (1 - q^(n+1))` is differentiable on the open unit disc. -/
+lemma differentiableOn_tprod_one_sub_pow :
+    DifferentiableOn ℂ (fun q ↦ ∏' n, (1 - q ^ (n + 1))) (Metric.ball (0 : ℂ) 1) :=
+  multipliableLocallyUniformlyOn_one_sub_pow.hasProdLocallyUniformlyOn.differentiableOn
+    (.of_forall fun _ ↦ by simpa [Finset.prod_fn] using
+      DifferentiableOn.finsetProd (fun _ _ ↦ by fun_prop)) Metric.isOpen_ball
+
+/-- For any `k`, the function `q ↦ ∏' n, (1 - q^(n+1))^k` is differentiable on the
+open unit disc. -/
+lemma differentiableOn_tprod_one_sub_pow_pow (k : ℕ) :
+    DifferentiableOn ℂ (fun q ↦ ∏' n, (1 - q ^ (n + 1)) ^ k) (Metric.ball (0 : ℂ) 1) :=
+  (differentiableOn_tprod_one_sub_pow.fun_pow k).congr fun _ hq ↦
+    (multipliable_one_sub_pow (by simpa using hq)).tprod_pow k
+
 theorem summable_eta_q (z : ℍ) : Summable fun n ↦ ‖-eta_q n z‖ := by
-  simp [eta_q, eta_q_eq_pow, summable_nat_add_iff 1, norm_exp_two_pi_I_lt_one z]
+  simpa [summable_nat_add_iff] using
+    summable_geometric_of_lt_one (norm_nonneg _) (mod_cast norm_qParam_lt_one 1 z)
 
 lemma multipliableLocallyUniformlyOn_eta :
-    MultipliableLocallyUniformlyOn (fun n a ↦ 1 - eta_q n a) ℍₒ := by
-  use fun z ↦ ∏' n, (1 - eta_q n z)
-  simp_rw [sub_eq_add_neg]
-  apply hasProdLocallyUniformlyOn_of_forall_compact isOpen_upperHalfPlaneSet
-  intro K hK hcK
-  by_cases hN : K.Nonempty
-  · have hc : ContinuousOn (fun x ↦ ‖cexp (2 * π * I * x)‖) K := by fun_prop
-    obtain ⟨z, hz, hB, HB⟩ := hcK.exists_sSup_image_eq_and_ge hN hc
-    apply (summable_eta_q ⟨z, hK hz⟩).hasProdUniformlyOn_nat_one_add hcK
-    · filter_upwards with n x hx
-      simpa [eta_q, eta_q_eq_pow] using pow_le_pow_left₀ (by simp [norm_nonneg]) (HB x hx) _
-    · simp_rw [eta_q, Periodic.qParam]
-      fun_prop
-  · rw [hasProdUniformlyOn_iff_tendstoUniformlyOn]
-    simpa [not_nonempty_iff_eq_empty.mp hN] using tendstoUniformlyOn_empty
+    MultipliableLocallyUniformlyOn (fun n a ↦ 1 - eta_q n a) ℍₒ :=
+  multipliableLocallyUniformlyOn_one_sub_pow.comp (𝕢 1)
+    (fun z hz ↦ by simpa using norm_qParam_lt_one 1 ⟨z, hz⟩) (by fun_prop)
 
 lemma eta_tprod_ne_zero {z : ℂ} (hz : z ∈ ℍₒ) : ∏' n, (1 - eta_q n z) ≠ 0 := by
   refine tprod_one_add_ne_zero_of_summable (f := fun n ↦ -eta_q n z) ?_ ?_
@@ -118,10 +144,9 @@ lemma tsum_logDeriv_eta_q (z : ℂ) : ∑' n, logDeriv (fun x ↦ 1 - eta_q n x)
 
 lemma differentiableAt_eta_tprod {z : ℂ} (hz : z ∈ ℍₒ) :
     DifferentiableAt ℂ (fun x ↦ ∏' n, (1 - eta_q n x)) z := by
-  apply (multipliableLocallyUniformlyOn_eta.hasProdLocallyUniformlyOn.differentiableOn ?_
-    isOpen_upperHalfPlaneSet z hz).differentiableAt (isOpen_upperHalfPlaneSet.mem_nhds hz)
-  filter_upwards with b
-  simpa [Finset.prod_fn] using DifferentiableOn.finsetProd (by fun_prop)
+  have hq : 𝕢 1 z ∈ Metric.ball 0 1 := by simpa using norm_qParam_lt_one 1 ⟨z, hz⟩
+  exact (differentiableOn_tprod_one_sub_pow.differentiableAt
+    (Metric.isOpen_ball.mem_nhds hq)).comp z (by fun_prop)
 
 theorem differentiableAt_eta_of_mem_upperHalfPlaneSet {z : ℂ} (hz : z ∈ ℍₒ) :
     DifferentiableAt ℂ eta z :=