Extension of invariant functions at a Fuchsian cusp

Let D be normalized cusp data for a subgroup of PSL(2, ℝ). Pulling a function on the upper half-plane back by D.scaling⁻¹ turns invariance under the cusp stabilizer into periodicity by D.width. Mathlib's periodic cusp function therefore descends the function to the punctured q-disc. If the original function is holomorphic at sufficiently large normalized heights and bounded as the scaled height tends to infinity, the descended function extends holomorphically across q = 0.

The construction uses the same q-coordinate as TauCeti.Subgroup.CuspDatum.qCoordinate. In particular, no choice of representatives of the stabilizer quotient occurs.

Main declarations

• TauCeti.Subgroup.CuspDatum.cuspExtension: the function of the q-variable, including its value at q = 0.
• TauCeti.Subgroup.CuspDatum.descend: its restriction to the punctured unit disc.
• TauCeti.Subgroup.CuspDatum.mdifferentiable_descend: an invariant holomorphic function descends holomorphically.
• TauCeti.Subgroup.CuspDatum.analyticAt_cuspExtension_zero: boundedness in the normalized scaling coordinate makes the singularity at q = 0 removable.

References

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

theorem TauCeti.Subgroup.CuspDatum.periodic_comp_ofComplex_inv_smul {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) (f : UpperHalfPlane → ℂ) (hf : ∀ (g : ↥(MulAction.stabilizer (↥Γ) D.cusp)) (z : UpperHalfPlane), f (g • z) = f z) : Function.Periodic ((fun (z : UpperHalfPlane) => f (D.scaling⁻¹ • z)) ∘ ↑UpperHalfPlane.ofComplex) ↑D.width

Pullback by the inverse scaling is periodic by the cusp width when a function is invariant under the full cusp stabilizer.

theorem TauCeti.Subgroup.CuspDatum.mdifferentiable_inv_smul {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) (f : UpperHalfPlane → ℂ) (hhol : MDiff f) : MDiff fun (z : UpperHalfPlane) => f (D.scaling⁻¹ • z)

Pulling a holomorphic function back by the inverse cusp scaling is holomorphic.

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

The function of the q-variable associated to a function on the upper half-plane and normalized cusp data. Away from zero it is obtained by a logarithmic lift in the scaling coordinate; its value at zero is Mathlib's limUnder extension.

Equations

• TauCeti.Subgroup.CuspDatum.cuspExtension D f = UpperHalfPlane.cuspFunction D.width fun (z : UpperHalfPlane) => f (D.scaling⁻¹ • z)

theorem TauCeti.Subgroup.CuspDatum.cuspExtension_def {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) (f : UpperHalfPlane → ℂ) : cuspExtension D f = UpperHalfPlane.cuspFunction D.width fun (z : UpperHalfPlane) => f (D.scaling⁻¹ • z)

The cusp extension is Mathlib's periodic cusp function applied after inverse scaling.

@[simp]

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

An invariant function is recovered by evaluating its cusp extension in the normalized q-coordinate.

noncomputable def TauCeti.Subgroup.CuspDatum.descend {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) (f : UpperHalfPlane → ℂ) : { q : Complex.UnitDisc // q ≠ 0 } → ℂ

The descent of a function to the punctured q-disc associated to normalized cusp data.

Equations

• TauCeti.Subgroup.CuspDatum.descend D f q = TauCeti.Subgroup.CuspDatum.cuspExtension D f ↑↑q

@[simp]

theorem TauCeti.Subgroup.CuspDatum.descend_apply {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) (f : UpperHalfPlane → ℂ) (q : { q : Complex.UnitDisc // q ≠ 0 }) : descend D f q = cuspExtension D f ↑↑q

The descended function is the restriction of the cusp extension to the punctured unit disc.

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

An invariant function is recovered by pulling its punctured-disc descent back along the normalized q-coordinate.

theorem TauCeti.Subgroup.CuspDatum.descend_unique {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) (f : UpperHalfPlane → ℂ) (hf : ∀ (g : ↥(MulAction.stabilizer (↥Γ) D.cusp)) (z : UpperHalfPlane), f (g • z) = f z) {F : { q : Complex.UnitDisc // q ≠ 0 } → ℂ} (hF : ∀ (z : UpperHalfPlane), F (qCoordinate D z) = f z) : F = descend D f

The descended function is the unique function on the punctured q-disc whose pullback along the normalized q-coordinate is the original invariant function.

theorem TauCeti.Subgroup.CuspDatum.differentiableAt_cuspExtension_of_ne_zero {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) (f : UpperHalfPlane → ℂ) (hf : ∀ (g : ↥(MulAction.stabilizer (↥Γ) D.cusp)) (z : UpperHalfPlane), f (g • z) = f z) (hhol : MDiff f) {q : ℂ} (hq : q ≠ 0) (hq_norm : ‖q‖ < 1) : DifferentiableAt ℂ (cuspExtension D f) q

The cusp extension of an invariant holomorphic function is complex differentiable at every nonzero point of the open unit disc.

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

An invariant holomorphic function descends to a holomorphic function on the punctured q-disc.

theorem TauCeti.Subgroup.CuspDatum.analyticAt_cuspExtension_zero {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) (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)) (hbounded : UpperHalfPlane.IsBoundedAtImInfty fun (z : UpperHalfPlane) => f (D.scaling⁻¹ • z)) : AnalyticAt ℂ (cuspExtension D f) 0

If an invariant function is holomorphic at all sufficiently large normalized heights and bounded as the normalized scaling coordinate tends to i∞, then its cusp extension is analytic at q = 0.

theorem TauCeti.Subgroup.CuspDatum.cuspExtension_zero_eq_valueAtInfty {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) (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)) (hbounded : UpperHalfPlane.IsBoundedAtImInfty fun (z : UpperHalfPlane) => f (D.scaling⁻¹ • z)) : cuspExtension D f 0 = UpperHalfPlane.valueAtInfty fun (z : UpperHalfPlane) => f (D.scaling⁻¹ • z)

For an invariant function holomorphic sufficiently high and bounded at the cusp, the value of its holomorphic extension at q = 0 is the limit of the function in the normalized scaling coordinate.

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

A bounded invariant holomorphic function approaches its cusp-extension value at the first q-exponential rate in the normalized scaling coordinate.

@[simp]

theorem TauCeti.Subgroup.CuspDatum.cuspExtension_zero_eq_zero {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) (f : UpperHalfPlane → ℂ) (hzero : UpperHalfPlane.IsZeroAtImInfty fun (z : UpperHalfPlane) => f (D.scaling⁻¹ • z)) : cuspExtension D f 0 = 0

If a function tends to zero in the normalized scaling coordinate, then the value of its cusp extension at q = 0 is zero.

theorem TauCeti.Subgroup.CuspDatum.isBigO_inv_smul_of_isZeroAtImInfty {Γ : Subgroup (Matrix.ProjectiveSpecialLinearGroup (Fin 2) ℝ)} (D : Γ.CuspDatum) (f : UpperHalfPlane → ℂ) (hf : ∀ (g : ↥(MulAction.stabilizer (↥Γ) D.cusp)) (z : UpperHalfPlane), f (g • z) = f z) (hhol : MDiff f) (hzero : UpperHalfPlane.IsZeroAtImInfty fun (z : UpperHalfPlane) => f (D.scaling⁻¹ • z)) : (fun (z : UpperHalfPlane) => f (D.scaling⁻¹ • z)) =O[UpperHalfPlane.atImInfty] fun (z : UpperHalfPlane) => Real.exp (-2 * Real.pi * z.im / D.width)

An invariant holomorphic function that tends to zero at the cusp does so at the first q-exponential rate in the normalized scaling coordinate.