Documentation

Mathlib.NumberTheory.ModularForms.QExpansion

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: #

source
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
source
theorem Function.Periodic.abs_qParam_le_of_one_half_le_im {ΞΎ : β„‚} (hΞΎ : 1 / 2 ≀ ΞΎ.im) :
β€–Function.Periodic.qParam 1 ΞΎβ€– ≀ Real.exp (-Real.pi)
source
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
source
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
    source
    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 Ο„
    source
    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
    source
    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)
    source
    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) :
    DifferentiableAt β„‚ (SlashInvariantFormClass.cuspFunction n f) q
    source
    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
    source
    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)
    source
    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
    source
    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)