Laurent expansions at a Fuchsian cusp #
Let D be normalized cusp data of width w, and suppose that an invariant holomorphic function
f grows no faster than exp (2 * π * k * y / w) in the scaling coordinate. Multiplication by
the k-th power of the q-coordinate gives a bounded holomorphic function. Its Taylor series at
zero, shifted down by k, is the Laurent expansion of f at the cusp.
This file packages that construction as a formal LaurentSeries ℂ. It proves that all
coefficients below exponent -k vanish and, more importantly, that the resulting Laurent series
converges to the descended function throughout the punctured unit disc. Thus the formal series is
connected to the actual quotient function rather than merely recording its coefficients. The
coefficients are uniquely characterized by this convergence together with the prescribed lower
support bound, so the resulting series is independent of the valid growth bound k used to
construct it.
Main declarations #
TauCeti.Subgroup.CuspDatum.twistedQExpansion: the Taylor series of the bounded twisted extension.TauCeti.Subgroup.CuspDatum.laurentQExpansion: that power series shifted by-k, as a formal Laurent series.TauCeti.Subgroup.CuspDatum.hasSum_laurentQExpansion: convergence of the Laurent expansion on the punctured q-disc.TauCeti.Subgroup.CuspDatum.hasSum_laurentQExpansion_coordinate: the corresponding expansion of the original function on the upper half-plane.TauCeti.Subgroup.CuspDatum.laurentQExpansion_coeff_unique: any convergent Laurent expansion supported in the prescribed range has these coefficients.TauCeti.Subgroup.CuspDatum.laurentQExpansion_eq: the expansion is independent of the valid growth bound used in its construction.
References #
- Fred Diamond and Jerry Shurman, A First Course in Modular Forms, §2.4.
- Otto Forster, Lectures on Riemann Surfaces, §19.
The Taylor series at zero of the q-extension obtained after twisting by q^k. Under the
hypotheses of hasSum_twistedQExpansion (invariance, holomorphy, and the growth bound for k),
this series converges on the open unit disc to twistedExtension D k f.
Equations
- TauCeti.Subgroup.CuspDatum.twistedQExpansion D k f = UpperHalfPlane.qExpansion D.width fun (z : UpperHalfPlane) => TauCeti.Subgroup.CuspDatum.cuspTwist D k f (D.scaling⁻¹ • z)
Instances For
The twisted q-expansion is Mathlib's q-expansion of the twist in the scaling coordinate.
The coefficients of the twisted q-expansion are the Taylor coefficients of the twisted extension at the cusp.
The constant coefficient of the twisted q-expansion is the value of the twisted extension at the cusp.
The Taylor series of the twisted extension, shifted by X⁻ᵏ, so that it is supported in
exponents at least -k. Under the growth bound for k, it is independent of k by
laurentQExpansion_eq.
Equations
Instances For
The Laurent q-expansion is the twisted q-expansion shifted down by k.
The coefficient of the Laurent q-expansion at an arbitrary integer exponent.
The coefficient of exponent n - k in the Laurent expansion is the n-th coefficient of
the Taylor series of the twisted extension.
There are no Laurent coefficients below the prescribed lower exponent -k.
The coefficient at the lowest permitted exponent is the value of the twisted extension at the cusp.
Under the exponential bound corresponding to k, the Taylor series of the twisted extension
converges to that extension at every point of the open unit disc.
The coefficient at the lowest permitted exponent -k is the limiting value of the twisted
function in the scaling coordinate.
The Laurent q-expansion converges to the cusp extension throughout the punctured unit disc, when reindexed over its potentially nonzero coefficients.
Reindex a Laurent q-expansion supported in exponents at least -k by n - k', for any
k' at least k.
The Laurent q-expansion, summed over all integer exponents, converges to the cusp extension throughout the punctured unit disc.
Pulling the Laurent q-expansion back by the normalized cusp coordinate gives the original function on the upper half-plane, when reindexed over its potentially nonzero coefficients.
Summing the Laurent q-expansion over every integer exponent after pullback by the normalized cusp coordinate gives the original function on the upper half-plane.
A Laurent series supported in exponents at least -k and converging to f in the cusp
coordinate has the coefficients of laurentQExpansion D k f.
Increasing a valid exponential growth rate does not change the Laurent q-expansion.
If k ≤ k', the coefficients of the Laurent expansion constructed using the k-bound,
reindexed by n - k', are the Taylor coefficients of the k'-twisted extension.
The Laurent q-expansion is independent of which valid exponential growth bound is used to construct it.