The order of a q-expansion under period rescaling #
The order of the q-expansion of a periodic, bounded, holomorphic function on the upper
half-plane equals the analytic order of its cuspFunction at 0; consequently, passing
from period h to period m * h multiplies the order by m. This is the vanishing-order
bookkeeping feeding the finite-index Sturm bound.
Main declarations #
TauCeti.qExpansion_order_eq_analyticOrderAt_cuspFunction.TauCeti.qExpansion_nat_mul_order:(qExpansion (m * h) g).order = (qExpansion h g).order * m.
References #
- Mathlib PR #39083 (Chris Birkbeck) — the upstream draft this file ports onto the current Mathlib pin.
theorem
TauCeti.qExpansion_order_eq_analyticOrderAt_cuspFunction
{h : ℝ}
{f : UpperHalfPlane → ℂ}
(hf : AnalyticAt ℂ (UpperHalfPlane.cuspFunction h f) 0)
:
The order of the q-expansion equals the analytic order of the cuspFunction at 0.
theorem
TauCeti.cuspFunction_nat_mul_eventuallyEq
{h : ℝ}
{g : UpperHalfPlane → ℂ}
{m : ℕ}
(hh : 0 < h)
(hm : 0 < m)
(hg_per : Function.Periodic (g ∘ ↑UpperHalfPlane.ofComplex) ↑h)
(hg_bdd : UpperHalfPlane.IsBoundedAtImInfty g)
(hg_mdiff : MDiff g)
:
UpperHalfPlane.cuspFunction (↑m * h) g =ᶠ[nhds 0] fun (q : ℂ) => UpperHalfPlane.cuspFunction h g (q ^ m)
The cusp function at period m * h agrees near 0 with the cusp function at period h
composed with the m-th power map.
theorem
TauCeti.qExpansion_nat_mul_order
{h : ℝ}
{g : UpperHalfPlane → ℂ}
{m : ℕ}
(hh : 0 < h)
(hm : 0 < m)
(hg_per : Function.Periodic (g ∘ ↑UpperHalfPlane.ofComplex) ↑h)
(hg_bdd : UpperHalfPlane.IsBoundedAtImInfty g)
(hg_mdiff : MDiff g)
:
The order of the q-expansion at period m * h is m times the order at period h.
theorem
TauCeti.qExpansion_order_le_qExpansion_nat_mul_order
{h : ℝ}
{g : UpperHalfPlane → ℂ}
{m : ℕ}
(hh : 0 < h)
(hm : 0 < m)
(hg_per : Function.Periodic (g ∘ ↑UpperHalfPlane.ofComplex) ↑h)
(hg_bdd : UpperHalfPlane.IsBoundedAtImInfty g)
(hg_mdiff : MDiff g)
:
The order of the q-expansion at period h is at most its order at period m * h.