feat(NumberTheory/ModularForms): q-expansions of modular forms (#18813)

Show that modular forms of level `n` can be written as analytic functions of `q = exp (2 * pi * I * z / n)`.



Co-authored-by: Chris Birkbeck <[email protected]>

Mathlib.lean

@@ -3782,6 +3782,7 @@ import Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
 import Mathlib.NumberTheory.ModularForms.JacobiTheta.Manifold
 import Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable
 import Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
+import Mathlib.NumberTheory.ModularForms.QExpansion
 import Mathlib.NumberTheory.ModularForms.SlashActions
 import Mathlib.NumberTheory.ModularForms.SlashInvariantForms
 import Mathlib.NumberTheory.MulChar.Basic

Mathlib/Analysis/Complex/Periodic.lean

@@ -20,7 +20,7 @@ for all sufficiently large `im z`, then `F` extends to a holomorphic function on
 to zero. These results are important in the theory of modular forms.
 -/
 
-open Complex Filter Asymptotics Function
+open Complex Filter Asymptotics
 
 open scoped Real Topology
 
@@ -30,6 +30,8 @@ local notation "I∞" => comap im atTop
 
 variable (h : ℝ)
 
+namespace Function.Periodic
+
 /-- Parameter for q-expansions, `qParam h z = exp (2 * π * I * z / h)` -/
 def qParam (z : ℂ) : ℂ := exp (2 * π * I * z / h)
 
@@ -214,3 +216,5 @@ theorem exp_decay_of_zero_at_inf (hh : 0 < h) (hf : Periodic f h)
       nhdsWithin_le_nhds
 
 end HoloAtInfC
+
+end Function.Periodic

Mathlib/Analysis/Complex/UpperHalfPlane/Basic.lean

@@ -104,6 +104,11 @@ theorem mk_im (z : ℂ) (h : 0 < z.im) : (mk z h).im = z.im :=
 theorem coe_mk (z : ℂ) (h : 0 < z.im) : (mk z h : ℂ) = z :=
   rfl
 
+@[simp]
+lemma coe_mk_subtype {z : ℂ} (hz : 0 < z.im) :
+    UpperHalfPlane.coe ⟨z, hz⟩ = z := by
+  rfl
+
 @[simp]
 theorem mk_coe (z : ℍ) (h : 0 < (z : ℂ).im := z.2) : mk z h = z :=
   rfl

Mathlib/Analysis/Complex/UpperHalfPlane/FunctionsBoundedAtInfty.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Chris Birkbeck, David Loeffler
 -/
 import Mathlib.Algebra.Module.Submodule.Basic
-import Mathlib.Analysis.Complex.UpperHalfPlane.Basic
+import Mathlib.Analysis.Complex.UpperHalfPlane.Topology
 import Mathlib.Order.Filter.ZeroAndBoundedAtFilter
 
 /-!
@@ -67,4 +67,17 @@ theorem zero_at_im_infty (f : ℍ → ℂ) :
   (atImInfty_basis.tendsto_iff Metric.nhds_basis_closedBall).trans <| by
     simp only [true_and, mem_closedBall_zero_iff]; rfl
 
+lemma tendsto_comap_im_ofComplex :
+    Tendsto ofComplex (comap Complex.im atTop) atImInfty := by
+  simp only [atImInfty, tendsto_comap_iff, Function.comp_def]
+  refine tendsto_comap.congr' ?_
+  filter_upwards [preimage_mem_comap (Ioi_mem_atTop 0)] with z hz
+  simp only [ofComplex_apply_of_im_pos hz, ← UpperHalfPlane.coe_im, coe_mk_subtype]
+
+lemma tendsto_coe_atImInfty :
+    Tendsto UpperHalfPlane.coe atImInfty (comap Complex.im atTop) := by
+  simpa only [atImInfty, tendsto_comap_iff, Function.comp_def,
+    funext UpperHalfPlane.coe_im] using tendsto_comap
+
+
 end UpperHalfPlane

Mathlib/Analysis/Complex/UpperHalfPlane/Manifold.lean

@@ -1,20 +1,21 @@
 /-
 Copyright (c) 2022 Chris Birkbeck. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Chris Birkbeck
+Authors: Chris Birkbeck, David Loeffler
 -/
 import Mathlib.Analysis.Complex.UpperHalfPlane.Topology
 import Mathlib.Geometry.Manifold.ContMDiff.Atlas
-import Mathlib.Geometry.Manifold.MFDeriv.Basic
+import Mathlib.Geometry.Manifold.MFDeriv.FDeriv
 
 /-!
 # Manifold structure on the upper half plane.
 
 In this file we define the complex manifold structure on the upper half-plane.
 -/
 
+open Filter
 
-open scoped UpperHalfPlane Manifold
+open scoped Manifold
 
 namespace UpperHalfPlane
 
@@ -31,4 +32,37 @@ theorem smooth_coe : Smooth 𝓘(ℂ) 𝓘(ℂ) ((↑) : ℍ → ℂ) := fun _ =
 theorem mdifferentiable_coe : MDifferentiable 𝓘(ℂ) 𝓘(ℂ) ((↑) : ℍ → ℂ) :=
   smooth_coe.mdifferentiable
 
+lemma smoothAt_ofComplex {z : ℂ} (hz : 0 < z.im) :
+    SmoothAt 𝓘(ℂ) 𝓘(ℂ) ofComplex z := by
+  rw [SmoothAt, contMDiffAt_iff]
+  constructor
+  · -- continuity at z
+    rw [ContinuousAt, nhds_induced, tendsto_comap_iff]
+    refine Tendsto.congr' (eventuallyEq_coe_comp_ofComplex hz).symm ?_
+    simpa only [ofComplex_apply_of_im_pos hz, Subtype.coe_mk] using tendsto_id
+  · -- smoothness in local chart
+    simp only [extChartAt, PartialHomeomorph.extend, modelWithCornersSelf_partialEquiv,
+      PartialEquiv.trans_refl, PartialHomeomorph.toFun_eq_coe, PartialHomeomorph.refl_partialEquiv,
+      PartialEquiv.refl_source, PartialHomeomorph.singletonChartedSpace_chartAt_eq,
+      PartialEquiv.refl_symm, PartialEquiv.refl_coe, CompTriple.comp_eq, modelWithCornersSelf_coe,
+      Set.range_id, id_eq, contDiffWithinAt_univ]
+    exact contDiffAt_id.congr_of_eventuallyEq (eventuallyEq_coe_comp_ofComplex hz)
+
+lemma mdifferentiableAt_ofComplex {z : ℂ} (hz : 0 < z.im) :
+    MDifferentiableAt 𝓘(ℂ) 𝓘(ℂ) ofComplex z :=
+  (smoothAt_ofComplex hz).mdifferentiableAt
+
+lemma mdifferentiableAt_iff {f : ℍ → ℂ} {τ : ℍ} :
+    MDifferentiableAt 𝓘(ℂ) 𝓘(ℂ) f τ ↔ DifferentiableAt ℂ (f ∘ ofComplex) ↑τ := by
+  rw [← mdifferentiableAt_iff_differentiableAt]
+  refine ⟨fun hf ↦ ?_, fun hf ↦ ?_⟩
+  · exact (ofComplex_apply τ ▸ hf).comp _ (mdifferentiableAt_ofComplex τ.im_pos)
+  · simpa only [Function.comp_def, ofComplex_apply] using hf.comp τ (mdifferentiable_coe τ)
+
+lemma mdifferentiable_iff {f : ℍ → ℂ} :
+    MDifferentiable 𝓘(ℂ) 𝓘(ℂ) f ↔ DifferentiableOn ℂ (f ∘ ofComplex) {z | 0 < z.im} :=
+  ⟨fun h z hz ↦ (mdifferentiableAt_iff.mp (h ⟨z, hz⟩)).differentiableWithinAt,
+    fun h ⟨z, hz⟩ ↦ mdifferentiableAt_iff.mpr <| (h z hz).differentiableAt
+      <| (Complex.continuous_im.isOpen_preimage _ isOpen_Ioi).mem_nhds hz⟩
+
 end UpperHalfPlane

Mathlib/Analysis/Complex/UpperHalfPlane/Topology.lean

@@ -121,12 +121,15 @@ theorem ModularGroup_T_zpow_mem_verticalStrip (z : ℍ) {N : ℕ} (hn : 0 < N) :
 
 end strips
 
-/-- A continuous section `ℂ → ℍ` of the natural inclusion map, bundled as a `PartialHomeomorph`. -/
+section ofComplex
+
+/-- A section `ℂ → ℍ` of the natural inclusion map, bundled as a `PartialHomeomorph`. -/
 def ofComplex : PartialHomeomorph ℂ ℍ := (isOpenEmbedding_coe.toPartialHomeomorph _).symm
 
 /-- Extend a function on `ℍ` arbitrarily to a function on all of `ℂ`. -/
 scoped notation "↑ₕ" f => f ∘ ofComplex
 
+@[simp]
 lemma ofComplex_apply (z : ℍ) : ofComplex (z : ℂ) = z :=
   IsOpenEmbedding.toPartialHomeomorph_left_inv ..
 
@@ -139,6 +142,10 @@ lemma ofComplex_apply_eq_ite (w : ℂ) :
     rintro ⟨a, rfl⟩
     exact (a.prop.not_le (by simpa using hw)).elim
 
+lemma ofComplex_apply_of_im_pos {z : ℂ} (hz : 0 < z.im) :
+    ofComplex z = ⟨z, hz⟩ := by
+  simpa only [coe_mk_subtype] using ofComplex_apply ⟨z, hz⟩
+
 lemma ofComplex_apply_of_im_nonpos {w : ℂ} (hw : w.im ≤ 0) :
     ofComplex w = Classical.choice inferInstance := by
   simp [ofComplex_apply_eq_ite w, hw]
@@ -157,4 +164,11 @@ lemma comp_ofComplex_of_im_le_zero (f : ℍ → ℂ) (z z' : ℂ) (hz : z.im ≤
     (↑ₕ f) z = (↑ₕ f) z' := by
   simp [ofComplex_apply_of_im_nonpos, hz, hz']
 
+lemma eventuallyEq_coe_comp_ofComplex {z : ℂ} (hz : 0 < z.im) :
+    UpperHalfPlane.coe ∘ ofComplex =ᶠ[𝓝 z] id := by
+  filter_upwards [(Complex.continuous_im.isOpen_preimage _ isOpen_Ioi).mem_nhds hz] with x hx
+  simp only [Function.comp_apply, ofComplex_apply_of_im_pos hx, id_eq, coe_mk_subtype]
+
+end ofComplex
+
 end UpperHalfPlane

Mathlib/NumberTheory/ModularForms/QExpansion.lean

@@ -0,0 +1,125 @@
+/-
+Copyright (c) 2024 David Loeffler. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: David Loeffler
+-/
+import Mathlib.Analysis.Complex.Periodic
+import Mathlib.NumberTheory.ModularForms.Basic
+import Mathlib.NumberTheory.ModularForms.Identities
+
+/-!
+# q-expansions of modular forms
+
+We show that a modular form of level `Γ(n)` can be written as `τ ↦ F (𝕢 n τ)` where `F` is
+analytic on the open unit disc, and `𝕢 n` is the parameter `τ ↦ exp (2 * I * π * τ / n)`. As an
+application, we show that cusp forms decay exponentially to 0 as `im τ → ∞`.
+
+## TO DO:
+
+* generalise to handle arbitrary finite-index subgroups (not just `Γ(n)` for some `n`)
+* define the `q`-expansion as a formal power series
+-/
+
+open ModularForm Complex Filter Asymptotics UpperHalfPlane Function
+
+open scoped Real Topology Manifold MatrixGroups CongruenceSubgroup
+
+noncomputable section
+
+variable {k : ℤ} {F : Type*} [FunLike F ℍ ℂ] {Γ : Subgroup SL(2, ℤ)} (n : ℕ) (f : F)
+
+local notation "I∞" => comap Complex.im atTop
+local notation "𝕢" => Periodic.qParam
+
+theorem Function.Periodic.im_invQParam_pos_of_abs_lt_one
+    {h : ℝ} (hh : 0 < h) {q : ℂ} (hq : q.abs < 1) (hq_ne : q ≠ 0) :
+    0 < im (Periodic.invQParam h q) :=
+  im_invQParam .. ▸ mul_pos_of_neg_of_neg
+    (div_neg_of_neg_of_pos (neg_lt_zero.mpr hh) Real.two_pi_pos)
+    ((Real.log_neg_iff (Complex.abs.pos hq_ne)).mpr hq)
+
+namespace SlashInvariantFormClass
+
+theorem periodic_comp_ofComplex [SlashInvariantFormClass F Γ(n) k] :
+    Periodic (f ∘ ofComplex) n := by
+  intro w
+  by_cases hw : 0 < im w
+  · have : 0 < im (w + n) := by simp only [add_im, natCast_im, add_zero, hw]
+    simp only [comp_apply, ofComplex_apply_of_im_pos this, ofComplex_apply_of_im_pos hw]
+    convert SlashInvariantForm.vAdd_width_periodic n k 1 f ⟨w, hw⟩ using 2
+    simp only [Int.cast_one, mul_one, UpperHalfPlane.ext_iff, coe_mk_subtype, coe_vadd,
+      ofReal_natCast, add_comm]
+  · have : im (w + n) ≤ 0 := by simpa only [add_im, natCast_im, add_zero, not_lt] using hw
+    simp only [comp_apply, ofComplex_apply_of_im_nonpos this,
+      ofComplex_apply_of_im_nonpos (not_lt.mp hw)]
+
+/--
+The analytic function `F` such that `f τ = F (exp (2 * π * I * τ / n))`, extended by a choice of
+limit at `0`.
+-/
+def cuspFunction : ℂ → ℂ := Function.Periodic.cuspFunction n (f ∘ ofComplex)
+
+theorem eq_cuspFunction [NeZero n] [SlashInvariantFormClass F Γ(n) k] (τ : ℍ) :
+    cuspFunction n f (𝕢 n τ) = f τ := by
+  simpa only [comp_apply, ofComplex_apply]
+    using (periodic_comp_ofComplex n f).eq_cuspFunction (NeZero.ne _) τ
+
+end SlashInvariantFormClass
+
+open SlashInvariantFormClass
+
+namespace ModularFormClass
+
+theorem differentiableAt_comp_ofComplex [ModularFormClass F Γ k] {z : ℂ} (hz : 0 < im z) :
+    DifferentiableAt ℂ (f ∘ ofComplex) z :=
+  mdifferentiableAt_iff_differentiableAt.mp ((holo f _).comp z (mdifferentiableAt_ofComplex hz))
+
+theorem bounded_at_infty_comp_ofComplex [ModularFormClass F Γ k] :
+    BoundedAtFilter I∞ (f ∘ ofComplex) := by
+  simpa only [SlashAction.slash_one, ModularForm.toSlashInvariantForm_coe]
+    using (ModularFormClass.bdd_at_infty f 1).comp_tendsto tendsto_comap_im_ofComplex
+
+theorem differentiableAt_cuspFunction [NeZero n] [ModularFormClass F Γ(n) k]
+    {q : ℂ} (hq : q.abs < 1) :
+    DifferentiableAt ℂ (cuspFunction n f) q := by
+  have npos : 0 < (n : ℝ) := mod_cast (Nat.pos_iff_ne_zero.mpr (NeZero.ne _))
+  rcases eq_or_ne q 0 with rfl | hq'
+  · exact (periodic_comp_ofComplex n f).differentiableAt_cuspFunction_zero npos
+      (eventually_of_mem (preimage_mem_comap (Ioi_mem_atTop 0))
+        (fun _ ↦ differentiableAt_comp_ofComplex f))
+      (bounded_at_infty_comp_ofComplex f)
+  · exact Periodic.qParam_right_inv npos.ne' hq' ▸
+      (periodic_comp_ofComplex n f).differentiableAt_cuspFunction npos.ne'
+        <| differentiableAt_comp_ofComplex _ <| Periodic.im_invQParam_pos_of_abs_lt_one npos hq hq'
+
+lemma analyticAt_cuspFunction_zero [NeZero n] [ModularFormClass F Γ(n) k] :
+    AnalyticAt ℂ (cuspFunction n f) 0 :=
+  DifferentiableOn.analyticAt
+    (fun q hq ↦ (differentiableAt_cuspFunction _ _ hq).differentiableWithinAt)
+    (by simpa only [ball_zero_eq] using Metric.ball_mem_nhds (0 : ℂ) zero_lt_one)
+
+end ModularFormClass
+
+open ModularFormClass
+
+namespace CuspFormClass
+
+theorem zero_at_infty_comp_ofComplex [CuspFormClass F Γ k] : ZeroAtFilter I∞ (f ∘ ofComplex) := by
+  simpa only [SlashAction.slash_one, toSlashInvariantForm_coe]
+    using (zero_at_infty f 1).comp tendsto_comap_im_ofComplex
+
+theorem cuspFunction_apply_zero [NeZero n] [CuspFormClass F Γ(n) k] :
+    cuspFunction n f 0 = 0 :=
+  Periodic.cuspFunction_zero_of_zero_at_inf (mod_cast (Nat.pos_iff_ne_zero.mpr (NeZero.ne _)))
+    (zero_at_infty_comp_ofComplex f)
+
+theorem exp_decay_atImInfty [NeZero n] [CuspFormClass F Γ(n) k] :
+    f =O[atImInfty] fun τ ↦ Real.exp (-2 * π * τ.im / n) := by
+  simpa only [neg_mul, comp_def, ofComplex_apply, coe_im] using
+    ((periodic_comp_ofComplex n f).exp_decay_of_zero_at_inf
+      (mod_cast (Nat.pos_iff_ne_zero.mpr (NeZero.ne _)))
+      (eventually_of_mem (preimage_mem_comap (Ioi_mem_atTop 0))
+        fun _ ↦ differentiableAt_comp_ofComplex f)
+      (zero_at_infty_comp_ofComplex f)).comp_tendsto tendsto_coe_atImInfty
+
+end CuspFormClass