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 somen) - define the
q-expansion as a formal power series
theorem
Function.Periodic.im_invQParam_pos_of_abs_lt_one
{h : ℝ}
(hh : 0 < h)
{q : ℂ}
(hq : Complex.abs q < 1)
(hq_ne : q ≠ 0)
:
0 < (Function.Periodic.invQParam h q).im
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
Instances For
theorem
SlashInvariantFormClass.eq_cuspFunction
{k : ℤ}
{F : Type u_1}
[FunLike F UpperHalfPlane ℂ]
(n : ℕ)
(f : F)
[NeZero n]
[SlashInvariantFormClass F (CongruenceSubgroup.Gamma n) k]
(τ : UpperHalfPlane)
:
SlashInvariantFormClass.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 : Complex.abs q < 1)
:
theorem
ModularFormClass.analyticAt_cuspFunction_zero
{k : ℤ}
{F : Type u_1}
[FunLike F UpperHalfPlane ℂ]
(n : ℕ)
(f : F)
[NeZero n]
[ModularFormClass F (CongruenceSubgroup.Gamma n) k]
:
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]
:
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)