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 τ → ∞.

We also define the q-expansion of a modular form, either as a power series or as a FormalMultlinearSeries, and show that it converges to f on the upper half plane.

Main definitions and results

• SlashInvariantFormClass.cuspFunction: for a level n slash-invariant form, this is the function F such that f τ = F (exp (2 * π * I * τ / n)), extended by a choice of limit at 0.
• ModularFormClass.differentiableAt_cuspFunction: when f is a modular form, its cuspFunction is differentiable on the open unit disc (including at 0).
• ModularFormClass.qExpansion: the q-expansion of a modular form (defined as the Taylor series of its cuspFunction), bundled as a PowerSeries.
• ModularFormClass.hasSum_qExpansion: the q-expansion evaluated at 𝕢 n τ sums to f τ, for τ in the upper half plane.

TO DO:

• generalise to handle arbitrary finite-index subgroups (not just Γ(n) for some n)
• define the q-expansion map on modular form spaces as a linear map (or even a ring hom from the graded ring of all modular forms?)

theorem SlashInvariantFormClass.periodic_comp_ofComplex {k : ℤ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] (n : ℕ) (f : F) [SlashInvariantFormClass F (CongruenceSubgroup.Gamma n) k] : Function.Periodic (⇑f ∘ ↑UpperHalfPlane.ofComplex) ↑n

def SlashInvariantFormClass.cuspFunction {F : Type u_1} [FunLike F UpperHalfPlane ℂ] (n : ℕ) (f : F) : ℂ → ℂ

The analytic function F such that f τ = F (exp (2 * π * I * τ / n)), extended by a choice of limit at 0.

Equations

• SlashInvariantFormClass.cuspFunction n f = Function.Periodic.cuspFunction (↑n) (⇑f ∘ ↑UpperHalfPlane.ofComplex)

theorem SlashInvariantFormClass.eq_cuspFunction {k : ℤ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] (n : ℕ) (f : F) [NeZero n] [SlashInvariantFormClass F (CongruenceSubgroup.Gamma n) k] (τ : UpperHalfPlane) : cuspFunction n f (Function.Periodic.qParam ↑n ↑τ) = f τ

theorem ModularFormClass.differentiableAt_comp_ofComplex {k : ℤ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} (f : F) [ModularFormClass F Γ k] {z : ℂ} (hz : 0 < z.im) : DifferentiableAt ℂ (⇑f ∘ ↑UpperHalfPlane.ofComplex) z

theorem ModularFormClass.bounded_at_infty_comp_ofComplex {k : ℤ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} (f : F) [ModularFormClass F Γ k] : (Filter.comap Complex.im Filter.atTop).BoundedAtFilter (⇑f ∘ ↑UpperHalfPlane.ofComplex)

theorem ModularFormClass.differentiableAt_cuspFunction {k : ℤ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] (n : ℕ) (f : F) [NeZero n] [ModularFormClass F (CongruenceSubgroup.Gamma n) k] {q : ℂ} (hq : ‖q‖ < 1) : DifferentiableAt ℂ (SlashInvariantFormClass.cuspFunction n f) q

theorem ModularFormClass.analyticAt_cuspFunction_zero {k : ℤ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] (n : ℕ) (f : F) [NeZero n] [ModularFormClass F (CongruenceSubgroup.Gamma n) k] : AnalyticAt ℂ (SlashInvariantFormClass.cuspFunction n f) 0

def ModularFormClass.qExpansion {F : Type u_1} [FunLike F UpperHalfPlane ℂ] (n : ℕ) (f : F) : PowerSeries ℂ

The q-expansion of a level n modular form, bundled as a PowerSeries.

Equations

• ModularFormClass.qExpansion n f = PowerSeries.mk fun (m : ℕ) => (↑m.factorial)⁻¹ * iteratedDeriv m (SlashInvariantFormClass.cuspFunction n f) 0

theorem ModularFormClass.qExpansion_coeff {F : Type u_1} [FunLike F UpperHalfPlane ℂ] (n : ℕ) (f : F) (m : ℕ) : (PowerSeries.coeff ℂ m) (qExpansion n f) = (↑m.factorial)⁻¹ * iteratedDeriv m (SlashInvariantFormClass.cuspFunction n f) 0

theorem ModularFormClass.hasSum_qExpansion_of_abs_lt {k : ℤ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] (n : ℕ) (f : F) [NeZero n] [ModularFormClass F (CongruenceSubgroup.Gamma n) k] {q : ℂ} (hq : ‖q‖ < 1) : HasSum (fun (m : ℕ) => (PowerSeries.coeff ℂ m) (qExpansion n f) • q ^ m) (SlashInvariantFormClass.cuspFunction n f q)

theorem ModularFormClass.hasSum_qExpansion {k : ℤ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] (n : ℕ) (f : F) [NeZero n] [ModularFormClass F (CongruenceSubgroup.Gamma n) k] (τ : UpperHalfPlane) : HasSum (fun (m : ℕ) => (PowerSeries.coeff ℂ m) (qExpansion n f) • Function.Periodic.qParam ↑n ↑τ ^ m) (f τ)

def ModularFormClass.qExpansionFormalMultilinearSeries {F : Type u_1} [FunLike F UpperHalfPlane ℂ] (n : ℕ) (f : F) : FormalMultilinearSeries ℂ ℂ ℂ

The q-expansion of a level n modular form, bundled as a FormalMultilinearSeries.

TODO: Maybe get rid of this and instead define a general API for converting PowerSeries to FormalMultlinearSeries.

Equations

• ModularFormClass.qExpansionFormalMultilinearSeries n f m = (PowerSeries.coeff ℂ m) (ModularFormClass.qExpansion n f) • ContinuousMultilinearMap.mkPiAlgebraFin ℂ m ℂ

theorem ModularFormClass.qExpansionFormalMultilinearSeries_apply_norm {F : Type u_1} [FunLike F UpperHalfPlane ℂ] (n : ℕ) (f : F) (m : ℕ) : ‖qExpansionFormalMultilinearSeries n f m‖ = ‖(PowerSeries.coeff ℂ m) (qExpansion n f)‖

theorem ModularFormClass.qExpansionFormalMultilinearSeries_radius {k : ℤ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] (n : ℕ) (f : F) [NeZero n] [ModularFormClass F (CongruenceSubgroup.Gamma n) k] : 1 ≤ (qExpansionFormalMultilinearSeries n f).radius

theorem ModularFormClass.hasFPowerSeries_cuspFunction {k : ℤ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] (n : ℕ) (f : F) [NeZero n] [ModularFormClass F (CongruenceSubgroup.Gamma n) k] : HasFPowerSeriesOnBall (SlashInvariantFormClass.cuspFunction n f) (qExpansionFormalMultilinearSeries n f) 0 1

The q-expansion of f is an FPowerSeries representing cuspFunction n f.

theorem CuspFormClass.zero_at_infty_comp_ofComplex {k : ℤ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} (f : F) [CuspFormClass F Γ k] : (Filter.comap Complex.im Filter.atTop).ZeroAtFilter (⇑f ∘ ↑UpperHalfPlane.ofComplex)

theorem CuspFormClass.cuspFunction_apply_zero {k : ℤ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] (n : ℕ) (f : F) [NeZero n] [CuspFormClass F (CongruenceSubgroup.Gamma n) k] : SlashInvariantFormClass.cuspFunction n f 0 = 0

theorem CuspFormClass.exp_decay_atImInfty {k : ℤ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] (n : ℕ) (f : F) [NeZero n] [CuspFormClass F (CongruenceSubgroup.Gamma n) k] : ⇑f =O[UpperHalfPlane.atImInfty] fun (τ : UpperHalfPlane) => Real.exp (-2 * Real.pi * τ.im / ↑n)