q-coefficient vanishing and cusp-function growth

The dictionary between vanishing of the first N q-coefficients of a periodic function on ℍ and O(‖q‖^N) growth of its cusp function at 0, in both directions, together with the limit of the function's values along Im τ → ∞. The general layer asks only for analyticity of the cusp function at 0 (with periodicity for the limit); the corollaries specialize to modular forms. These are the analytic inputs of the norm step of the general-level valence reduction: growth bounds are multiplicative, so they transport coefficient vanishing through the norm map to level one.

Main declarations

• TauCeti.UpperHalfPlane.cuspFunction_isBigO_pow_of_qExpansion_coeff_eq_zero and TauCeti.UpperHalfPlane.qExpansion_coeff_eq_zero_of_cuspFunction_isBigO_pow: the two directions of the dictionary, for any function whose cusp function is analytic at 0.
• TauCeti.UpperHalfPlane.tendsto_valueAtInfty: an h-periodic function with cusp function analytic at 0 tends to valueAtInfty along atImInfty.
• The TauCeti.ModularFormClass corollaries of all three, for a modular form on a subgroup with h in its strict period set.

References

Ported from AINTLIB's LeanModularForms project (github.com/CBirkbeck/AINTLIB, commit 2baa76f742, Apache 2.0, the file projects/LeanModularForms/LeanModularForms/Modularforms/DimGenCongLevels/Auxiliary.lean), generalized to the function level and reproved through Mathlib's power-series uniqueness machinery instead of the source's circle-integral bounds.

theorem TauCeti.UpperHalfPlane.tendsto_valueAtInfty {h : ℝ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {f : F} (hh : 0 < h) (hper : Function.Periodic (⇑f ∘ ↑UpperHalfPlane.ofComplex) ↑h) (hfanalytic : AnalyticAt ℂ (UpperHalfPlane.cuspFunction h ⇑f) 0) : Filter.Tendsto (fun (τ : UpperHalfPlane) => f τ) UpperHalfPlane.atImInfty (nhds (UpperHalfPlane.valueAtInfty ⇑f))

A function on ℍ that is h-periodic with cusp function analytic at 0 tends to valueAtInfty along atImInfty.

theorem TauCeti.UpperHalfPlane.cuspFunction_isBigO_pow_of_qExpansion_coeff_eq_zero {h : ℝ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {f : F} (hfanalytic : AnalyticAt ℂ (UpperHalfPlane.cuspFunction h ⇑f) 0) (N : ℕ) (hcoeff : ∀ n < N, (PowerSeries.coeff n) (UpperHalfPlane.qExpansion h ⇑f) = 0) : UpperHalfPlane.cuspFunction h ⇑f =O[nhds 0] fun (q : ℂ) => ‖q‖ ^ N

If the first N q-coefficients vanish, then the cusp function is O(‖q‖^N) near 0.

theorem TauCeti.UpperHalfPlane.qExpansion_coeff_eq_zero_of_cuspFunction_isBigO_pow {h : ℝ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {f : F} (hfanalytic : AnalyticAt ℂ (UpperHalfPlane.cuspFunction h ⇑f) 0) {N n : ℕ} (hn : n < N) (hO : UpperHalfPlane.cuspFunction h ⇑f =O[nhds 0] fun (q : ℂ) => ‖q‖ ^ N) : (PowerSeries.coeff n) (UpperHalfPlane.qExpansion h ⇑f) = 0

If cuspFunction h f = O(‖q‖^N) near 0, then the n-th q-coefficient vanishes for n < N.

theorem TauCeti.ModularFormClass.tendsto_valueAtInfty {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} {h : ℝ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] [ModularFormClass F Γ k] (f : F) (hh : 0 < h) (hΓ : h ∈ Γ.strictPeriods) : Filter.Tendsto (fun (τ : UpperHalfPlane) => f τ) UpperHalfPlane.atImInfty (nhds (UpperHalfPlane.valueAtInfty ⇑f))

Values of a modular form tend to valueAtInfty along atImInfty.

theorem TauCeti.ModularFormClass.cuspFunction_isBigO_pow_of_qExpansion_coeff_eq_zero {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} {h : ℝ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] [ModularFormClass F Γ k] (f : F) (hh : 0 < h) (hΓ : h ∈ Γ.strictPeriods) (N : ℕ) (hcoeff : ∀ n < N, (PowerSeries.coeff n) (UpperHalfPlane.qExpansion h ⇑f) = 0) : UpperHalfPlane.cuspFunction h ⇑f =O[nhds 0] fun (q : ℂ) => ‖q‖ ^ N

If the first N q-coefficients of a modular form vanish, then its cusp function is O(‖q‖^N) near 0.

theorem TauCeti.ModularFormClass.qExpansion_coeff_eq_zero_of_cuspFunction_isBigO_pow {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} {h : ℝ} {F : Type u_1} [FunLike F UpperHalfPlane ℂ] [ModularFormClass F Γ k] (f : F) (hh : 0 < h) (hΓ : h ∈ Γ.strictPeriods) {N n : ℕ} (hn : n < N) (hO : UpperHalfPlane.cuspFunction h ⇑f =O[nhds 0] fun (q : ℂ) => ‖q‖ ^ N) : (PowerSeries.coeff n) (UpperHalfPlane.qExpansion h ⇑f) = 0

If the cusp function of a modular form is O(‖q‖^N) near 0, then its n-th q-coefficient vanishes for n < N.