Meromorphic extension of functions of controlled growth at a cusp

Let D be normalized cusp data of width w. If an invariant function is holomorphic at sufficiently large normalized heights and grows no faster than exp (2 * π * n * y / w) in the scaling coordinate, multiplication by q^n makes it bounded. The removable-singularity theorem then gives an analytic numerator in the q-coordinate, so the original function extends meromorphically with pole order at most n.

The integer-indexed twistedExtension D k f treats poles and zeros uniformly. Positive k cancels growth by multiplying by q^k, while negative k cancels decay by dividing by a power of q. This also makes the relevant coefficient available to later q-expansion and local-order arguments.

Main declarations

• TauCeti.Subgroup.CuspDatum.twistedExtension: the q-extension after an integer coordinate twist.
• TauCeti.Subgroup.CuspDatum.analyticAt_twistedExtension_zero: the matching exponential bound makes that extension analytic at the cusp.
• TauCeti.Subgroup.CuspDatum.meromorphicAt_cuspExtension_zero: the original q-extension is meromorphic at zero.
• TauCeti.Subgroup.CuspDatum.neg_natCast_le_meromorphicOrderAt_cuspExtension: its order is at least -n, equivalently its pole order is at most n.
• TauCeti.Subgroup.CuspDatum.natCast_le_meromorphicOrderAt_cuspExtension: exponential decay of order n forces the cusp extension to have order at least n.

References

• Fred Diamond and Jerry Shurman, A First Course in Modular Forms, §2.4.
• Otto Forster, Lectures on Riemann Surfaces, §19.

noncomputable def TauCeti.Subgroup.CuspDatum.cuspTwist {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) (k : ℤ) (f : UpperHalfPlane → ℂ) : UpperHalfPlane → ℂ

Multiplication by an integer power of the cusp coordinate before descent.

Equations

• TauCeti.Subgroup.CuspDatum.cuspTwist D k f z = TauCeti.Subgroup.CuspDatum.coordinate D z ^ k * f z

@[simp]

theorem TauCeti.Subgroup.CuspDatum.cuspTwist_apply {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) (k : ℤ) (f : UpperHalfPlane → ℂ) (z : UpperHalfPlane) : cuspTwist D k f z = coordinate D z ^ k * f z

The cusp twist is pointwise multiplication by the corresponding integer power of the q-coordinate.

theorem TauCeti.Subgroup.CuspDatum.cuspTwist_smul {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) (k : ℤ) (f : UpperHalfPlane → ℂ) (hf : ∀ (g : ↥(MulAction.stabilizer (↥Γ) D.cusp)) (z : UpperHalfPlane), f (g • z) = f z) (g : ↥(MulAction.stabilizer (↥Γ) D.cusp)) (z : UpperHalfPlane) : cuspTwist D k f (g • z) = cuspTwist D k f z

Twisting preserves invariance under the full cusp stabilizer.

theorem TauCeti.Subgroup.CuspDatum.mdifferentiableAt_cuspTwist {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) (k : ℤ) (f : UpperHalfPlane → ℂ) (z : UpperHalfPlane) (hf : MDiffAt f z) : MDiffAt (cuspTwist D k f) z

Twisting by an integer power of the nonvanishing cusp coordinate preserves holomorphy at any point where the original function is holomorphic.

theorem TauCeti.Subgroup.CuspDatum.mdifferentiable_cuspTwist {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) (k : ℤ) (f : UpperHalfPlane → ℂ) (hf : MDiff f) : MDiff (cuspTwist D k f)

Twisting a holomorphic function by an integer power of the nonvanishing cusp coordinate preserves holomorphy.

theorem TauCeti.Subgroup.CuspDatum.cuspTwist_inv_smul {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) (k : ℤ) (f : UpperHalfPlane → ℂ) (z : UpperHalfPlane) : cuspTwist D k f (D.scaling⁻¹ • z) = Function.Periodic.qParam D.width ↑z ^ k * f (D.scaling⁻¹ • z)

In the normalized scaling coordinate, twisting is multiplication by the usual width-w q-parameter.

theorem TauCeti.Subgroup.CuspDatum.isBoundedAtImInfty_cuspTwist_inv_smul {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) (k : ℤ) (f : UpperHalfPlane → ℂ) (hbound : (fun (z : UpperHalfPlane) => f (D.scaling⁻¹ • z)) =O[UpperHalfPlane.atImInfty] fun (z : UpperHalfPlane) => Real.exp (2 * Real.pi * ↑k * z.im / D.width)) : UpperHalfPlane.IsBoundedAtImInfty fun (z : UpperHalfPlane) => cuspTwist D k f (D.scaling⁻¹ • z)

Multiplying by the cusp coordinate to the power k cancels the corresponding exponential growth in the scaling coordinate. In particular, the twisted function is bounded at the cusp.

noncomputable def TauCeti.Subgroup.CuspDatum.twistedExtension {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) (k : ℤ) (f : UpperHalfPlane → ℂ) : ℂ → ℂ

The q-extension after twisting by an integer power of the cusp coordinate. Under the corresponding hypothesis of analyticAt_twistedExtension_zero, it is analytic at zero.

Equations

• TauCeti.Subgroup.CuspDatum.twistedExtension D k f = TauCeti.Subgroup.CuspDatum.cuspExtension D (TauCeti.Subgroup.CuspDatum.cuspTwist D k f)

theorem TauCeti.Subgroup.CuspDatum.twistedExtension_def {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) (k : ℤ) (f : UpperHalfPlane → ℂ) : twistedExtension D k f = cuspExtension D (cuspTwist D k f)

The twisted extension is the cusp extension of the coordinate-twisted function.

@[simp]

theorem TauCeti.Subgroup.CuspDatum.twistedExtension_coordinate {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) (k : ℤ) (f : UpperHalfPlane → ℂ) (hf : ∀ (g : ↥(MulAction.stabilizer (↥Γ) D.cusp)) (z : UpperHalfPlane), f (g • z) = f z) (z : UpperHalfPlane) : twistedExtension D k f (coordinate D z) = coordinate D z ^ k * f z

Pulling the twisted extension back along the cusp coordinate recovers q^k f.

theorem TauCeti.Subgroup.CuspDatum.analyticAt_twistedExtension_zero {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) (k : ℤ) (f : UpperHalfPlane → ℂ) (hf : ∀ (g : ↥(MulAction.stabilizer (↥Γ) D.cusp)) (z : UpperHalfPlane), f (g • z) = f z) (hhol : ∀ᶠ (z : UpperHalfPlane) in UpperHalfPlane.atImInfty, MDiffAt f (D.scaling⁻¹ • z)) (hbound : (fun (z : UpperHalfPlane) => f (D.scaling⁻¹ • z)) =O[UpperHalfPlane.atImInfty] fun (z : UpperHalfPlane) => Real.exp (2 * Real.pi * ↑k * z.im / D.width)) : AnalyticAt ℂ (twistedExtension D k f) 0

The exponential bound corresponding to the integer twist k makes the twisted q-extension analytic at zero.

theorem TauCeti.Subgroup.CuspDatum.twistedExtension_zero_eq_valueAtInfty {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) (k : ℤ) (f : UpperHalfPlane → ℂ) (hf : ∀ (g : ↥(MulAction.stabilizer (↥Γ) D.cusp)) (z : UpperHalfPlane), f (g • z) = f z) (hhol : ∀ᶠ (z : UpperHalfPlane) in UpperHalfPlane.atImInfty, MDiffAt f (D.scaling⁻¹ • z)) (hbound : (fun (z : UpperHalfPlane) => f (D.scaling⁻¹ • z)) =O[UpperHalfPlane.atImInfty] fun (z : UpperHalfPlane) => Real.exp (2 * Real.pi * ↑k * z.im / D.width)) : twistedExtension D k f 0 = UpperHalfPlane.valueAtInfty fun (z : UpperHalfPlane) => Function.Periodic.qParam D.width ↑z ^ k * f (D.scaling⁻¹ • z)

The value at zero of the twisted extension is the value at infinity of the twisted function in the normalized scaling coordinate.

theorem TauCeti.Subgroup.CuspDatum.cuspExtension_eq_zpow_mul_twistedExtension_of_ne_zero_of_norm_lt_one {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) (k : ℤ) (f : UpperHalfPlane → ℂ) (hf : ∀ (g : ↥(MulAction.stabilizer (↥Γ) D.cusp)) (z : UpperHalfPlane), f (g • z) = f z) {q : ℂ} (hq : q ≠ 0) (hq_norm : ‖q‖ < 1) : cuspExtension D f q = q ^ (-k) * twistedExtension D k f q

On the punctured unit disc, the original cusp extension is q⁻ᵏ times its twisted extension.

theorem TauCeti.Subgroup.CuspDatum.cuspExtension_eventuallyEq_zpow_mul_twistedExtension {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) (k : ℤ) (f : UpperHalfPlane → ℂ) (hf : ∀ (g : ↥(MulAction.stabilizer (↥Γ) D.cusp)) (z : UpperHalfPlane), f (g • z) = f z) : cuspExtension D f =ᶠ[nhdsWithin 0 {0}ᶜ] fun (q : ℂ) => q ^ (-k) * twistedExtension D k f q

Near the puncture, the original cusp extension is q⁻ᵏ times its twisted extension.

theorem TauCeti.Subgroup.CuspDatum.meromorphicAt_cuspExtension_zero {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) (k : ℤ) (f : UpperHalfPlane → ℂ) (hf : ∀ (g : ↥(MulAction.stabilizer (↥Γ) D.cusp)) (z : UpperHalfPlane), f (g • z) = f z) (hhol : ∀ᶠ (z : UpperHalfPlane) in UpperHalfPlane.atImInfty, MDiffAt f (D.scaling⁻¹ • z)) (hbound : (fun (z : UpperHalfPlane) => f (D.scaling⁻¹ • z)) =O[UpperHalfPlane.atImInfty] fun (z : UpperHalfPlane) => Real.exp (2 * Real.pi * ↑k * z.im / D.width)) : MeromorphicAt (cuspExtension D f) 0

A cusp-invariant function holomorphic sufficiently high and satisfying the exponential bound for an integer twist has a meromorphic q-extension at the cusp.

theorem TauCeti.Subgroup.CuspDatum.neg_le_meromorphicOrderAt_cuspExtension {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) (k : ℤ) (f : UpperHalfPlane → ℂ) (hf : ∀ (g : ↥(MulAction.stabilizer (↥Γ) D.cusp)) (z : UpperHalfPlane), f (g • z) = f z) (hhol : ∀ᶠ (z : UpperHalfPlane) in UpperHalfPlane.atImInfty, MDiffAt f (D.scaling⁻¹ • z)) (hbound : (fun (z : UpperHalfPlane) => f (D.scaling⁻¹ • z)) =O[UpperHalfPlane.atImInfty] fun (z : UpperHalfPlane) => Real.exp (2 * Real.pi * ↑k * z.im / D.width)) : ↑(-k) ≤ meromorphicOrderAt (cuspExtension D f) 0

The meromorphic order of a cusp extension is at least -k under the exponential bound corresponding to the integer coordinate twist k.

theorem TauCeti.Subgroup.CuspDatum.neg_natCast_le_meromorphicOrderAt_cuspExtension {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) (n : ℕ) (f : UpperHalfPlane → ℂ) (hf : ∀ (g : ↥(MulAction.stabilizer (↥Γ) D.cusp)) (z : UpperHalfPlane), f (g • z) = f z) (hhol : ∀ᶠ (z : UpperHalfPlane) in UpperHalfPlane.atImInfty, MDiffAt f (D.scaling⁻¹ • z)) (hgrowth : (fun (z : UpperHalfPlane) => f (D.scaling⁻¹ • z)) =O[UpperHalfPlane.atImInfty] fun (z : UpperHalfPlane) => Real.exp (2 * Real.pi * ↑n * z.im / D.width)) : -↑↑n ≤ meromorphicOrderAt (cuspExtension D f) 0

Exponential growth of rate at most 2πn / w forces the meromorphic order of the cusp extension to be at least -n; equivalently, its pole order is at most n.

Controlled zeros

theorem TauCeti.Subgroup.CuspDatum.analyticAt_cuspExtension_zero_of_isBigO_exp_neg {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) (n : ℕ) (f : UpperHalfPlane → ℂ) (hf : ∀ (g : ↥(MulAction.stabilizer (↥Γ) D.cusp)) (z : UpperHalfPlane), f (g • z) = f z) (hhol : ∀ᶠ (z : UpperHalfPlane) in UpperHalfPlane.atImInfty, MDiffAt f (D.scaling⁻¹ • z)) (hdecay : (fun (z : UpperHalfPlane) => f (D.scaling⁻¹ • z)) =O[UpperHalfPlane.atImInfty] fun (z : UpperHalfPlane) => Real.exp (-2 * Real.pi * ↑n * z.im / D.width)) : AnalyticAt ℂ (cuspExtension D f) 0

A cusp-invariant function holomorphic sufficiently high with exponential decay of order n has a holomorphic q-extension at the cusp.

theorem TauCeti.Subgroup.CuspDatum.natCast_le_meromorphicOrderAt_cuspExtension {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) (n : ℕ) (f : UpperHalfPlane → ℂ) (hf : ∀ (g : ↥(MulAction.stabilizer (↥Γ) D.cusp)) (z : UpperHalfPlane), f (g • z) = f z) (hhol : ∀ᶠ (z : UpperHalfPlane) in UpperHalfPlane.atImInfty, MDiffAt f (D.scaling⁻¹ • z)) (hdecay : (fun (z : UpperHalfPlane) => f (D.scaling⁻¹ • z)) =O[UpperHalfPlane.atImInfty] fun (z : UpperHalfPlane) => Real.exp (-2 * Real.pi * ↑n * z.im / D.width)) : ↑↑n ≤ meromorphicOrderAt (cuspExtension D f) 0

Exponential decay of rate at least 2πn / w forces the meromorphic order of the cusp extension to be at least n; equivalently, the extension has a zero of order at least n.