The local coordinate at a cusp

For a positive width w, the usual local coordinate z ↦ exp (2 π i z / w) maps the upper half-plane onto the punctured unit disc. Its fibres are exactly the orbits of the translation subgroup w ℤ. Consequently it identifies the orbit quotient of the upper half-plane by these translations with the punctured unit disc.

A periodic function need only be holomorphic above some height for boundedness to make its q-extension analytic at zero. This permits applying the same coordinate to functions with interior poles.

The construction reuses Mathlib's Function.Periodic.qParam; in particular, the normalization of 2 π i / w agrees with the local parameter used for modular-form q-expansions. The analytic extension criterion uses Function.Periodic.differentiableAt_cuspFunction_zero and Mathlib's removable singularity theorem.

Main declarations

• TauCeti.UpperHalfPlane.qParamPuncturedUnitDisc: the width-w q-parameter with its range bundled.
• TauCeti.UpperHalfPlane.invQParamUpperHalfPlane: a chosen logarithmic lift/right inverse, valued in the upper half-plane.
• TauCeti.UpperHalfPlane.qParamPuncturedUnitDisc_eq_iff: two lifts have the same q-parameter exactly when they differ by an integral multiple of the width.
• TauCeti.UpperHalfPlane.cuspTranslationQuotientHomeomorph: the resulting homeomorphism from the translation-orbit quotient to the punctured unit disc.
• TauCeti.UpperHalfPlane.analyticAt_cuspFunction_zero_of_eventually_mdifferentiableAt: bounded functions holomorphic sufficiently high have a removable q-singularity.

References

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

theorem TauCeti.UpperHalfPlane.analyticAt_cuspFunction_zero_of_eventually_mdifferentiableAt {f : UpperHalfPlane → ℂ} {w : ℝ} (hw : 0 < w) (hper : Function.Periodic (f ∘ ↑UpperHalfPlane.ofComplex) ↑w) (hhol : ∀ᶠ (z : UpperHalfPlane) in UpperHalfPlane.atImInfty, MDiffAt f z) (hbounded : UpperHalfPlane.IsBoundedAtImInfty f) : AnalyticAt ℂ (Function.Periodic.cuspFunction w (f ∘ ↑UpperHalfPlane.ofComplex)) 0

A periodic function holomorphic at all sufficiently large heights and bounded at imaginary infinity has an analytic q-extension at zero. Interior poles below that height are allowed.

noncomputable def TauCeti.UpperHalfPlane.qParamPuncturedUnitDisc (w : ℝ) (hw : 0 < w) (z : UpperHalfPlane) : { q : Complex.UnitDisc // q ≠ 0 }

The q-parameter of positive width, regarded as a map from the upper half-plane to the punctured unit disc.

Equations

• TauCeti.UpperHalfPlane.qParamPuncturedUnitDisc w hw z = ⟨Complex.UnitDisc.mk (Function.Periodic.qParam w ↑z) ⋯, ⋯⟩

@[simp]

theorem TauCeti.UpperHalfPlane.coe_qParamPuncturedUnitDisc (w : ℝ) (hw : 0 < w) (z : UpperHalfPlane) : ↑↑(qParamPuncturedUnitDisc w hw z) = Function.Periodic.qParam w ↑z

noncomputable def TauCeti.UpperHalfPlane.invQParamUpperHalfPlane (w : ℝ) (hw : 0 < w) (q : { q : Complex.UnitDisc // q ≠ 0 }) : UpperHalfPlane

The logarithmic lift of a point of the punctured unit disc to the upper half-plane.

Equations

• TauCeti.UpperHalfPlane.invQParamUpperHalfPlane w hw q = { coe := Function.Periodic.invQParam w ↑↑q, coe_im_pos := ⋯ }

@[simp]

theorem TauCeti.UpperHalfPlane.coe_invQParamUpperHalfPlane (w : ℝ) (hw : 0 < w) (q : { q : Complex.UnitDisc // q ≠ 0 }) : ↑(invQParamUpperHalfPlane w hw q) = Function.Periodic.invQParam w ↑↑q

@[simp]

theorem TauCeti.UpperHalfPlane.qParamPuncturedUnitDisc_invQParamUpperHalfPlane (w : ℝ) (hw : 0 < w) (q : { q : Complex.UnitDisc // q ≠ 0 }) : qParamPuncturedUnitDisc w hw (invQParamUpperHalfPlane w hw q) = q

theorem TauCeti.UpperHalfPlane.qParamPuncturedUnitDisc_surjective (w : ℝ) (hw : 0 < w) : Function.Surjective (qParamPuncturedUnitDisc w hw)

Every nonzero point of the unit disc has a logarithmic lift to the upper half-plane.

theorem TauCeti.UpperHalfPlane.mdifferentiable_qParamPuncturedUnitDisc (w : ℝ) (hw : 0 < w) : MDiff (qParamPuncturedUnitDisc w hw)

The q-parameter is holomorphic as a map into the punctured unit disc.

theorem TauCeti.UpperHalfPlane.norm_qParamPuncturedUnitDisc_lt_iff (w : ℝ) (hw : 0 < w) (A : ℝ) (z : UpperHalfPlane) : ‖↑↑(qParamPuncturedUnitDisc w hw z)‖ < Real.exp (-2 * Real.pi * A / w) ↔ A < z.im

A horodisc is the inverse image of the punctured disc of the corresponding radius.

theorem TauCeti.UpperHalfPlane.image_qParamPuncturedUnitDisc_setOf_lt_im (w : ℝ) (hw : 0 < w) (A : ℝ) : qParamPuncturedUnitDisc w hw '' {z : UpperHalfPlane | A < z.im} = {q : { q : Complex.UnitDisc // q ≠ 0 } | ‖↑↑q‖ < Real.exp (-2 * Real.pi * A / w)}

The image of a horodisc is the punctured disc of the corresponding exponential radius.

theorem TauCeti.UpperHalfPlane.tendsto_qParamPuncturedUnitDisc (w : ℝ) (hw : 0 < w) : Filter.Tendsto (fun (z : UpperHalfPlane) => ↑↑(qParamPuncturedUnitDisc w hw z)) UpperHalfPlane.atImInfty (nhdsWithin 0 {0}ᶜ)

The q-parameter tends to zero through nonzero values as the height tends to infinity.

theorem TauCeti.UpperHalfPlane.isBoundedAtImInfty_qParam_zpow_mul_of_isBigO (w : ℝ) (k : ℤ) {f : UpperHalfPlane → ℂ} (hf : f =O[UpperHalfPlane.atImInfty] fun (z : UpperHalfPlane) => Real.exp (2 * Real.pi * ↑k * z.im / w)) : UpperHalfPlane.IsBoundedAtImInfty fun (z : UpperHalfPlane) => Function.Periodic.qParam w ↑z ^ k * f z

Multiplying by the kth integer power of the q-parameter cancels the opposing exponential comparison and gives a function bounded at i∞. For positive width, nonnegative k controls growth, while negative k controls decay.

theorem TauCeti.UpperHalfPlane.qParamPuncturedUnitDisc_eq_iff (w : ℝ) (hw : 0 < w) (z z' : UpperHalfPlane) : qParamPuncturedUnitDisc w hw z = qParamPuncturedUnitDisc w hw z' ↔ ∃ (n : ℤ), z = ↑n * w +ᵥ z'

Two points of the upper half-plane have the same width-w q-parameter exactly when one is an integral-width translate of the other.

@[reducible, inline]

abbrev TauCeti.UpperHalfPlane.CuspTranslationQuotient (w : ℝ) : Type

The orbit quotient of the upper half-plane by translations through integral multiples of a positive width.

Equations

• TauCeti.UpperHalfPlane.CuspTranslationQuotient w = AddAction.orbitRel.Quotient (↥(AddSubgroup.zmultiples w)) UpperHalfPlane

theorem TauCeti.UpperHalfPlane.cuspTranslationOrbitRel_iff_qParam_eq (w : ℝ) (hw : 0 < w) (z z' : UpperHalfPlane) : (AddAction.orbitRel (↥(AddSubgroup.zmultiples w)) UpperHalfPlane) z z' ↔ qParamPuncturedUnitDisc w hw z = qParamPuncturedUnitDisc w hw z'

The orbit relation for integral-width translations is exactly equality of q-parameters.

theorem TauCeti.UpperHalfPlane.isOpenQuotientMap_qParamPuncturedUnitDisc (w : ℝ) (hw : 0 < w) : IsOpenQuotientMap (qParamPuncturedUnitDisc w hw)

The q-parameter from the upper half-plane to the punctured unit disc is an open quotient map.

noncomputable def TauCeti.UpperHalfPlane.cuspTranslationQuotientMap (w : ℝ) (hw : 0 < w) : CuspTranslationQuotient w → { q : Complex.UnitDisc // q ≠ 0 }

The q-parameter descended to the width-translation quotient.

Equations

• TauCeti.UpperHalfPlane.cuspTranslationQuotientMap w hw = Quotient.lift (TauCeti.UpperHalfPlane.qParamPuncturedUnitDisc w hw) ⋯

@[simp]

theorem TauCeti.UpperHalfPlane.cuspTranslationQuotientMap_mk (w : ℝ) (hw : 0 < w) (z : UpperHalfPlane) : cuspTranslationQuotientMap w hw (Quotient.mk'' z) = qParamPuncturedUnitDisc w hw z

theorem TauCeti.UpperHalfPlane.isHomeomorph_cuspTranslationQuotientMap (w : ℝ) (hw : 0 < w) : IsHomeomorph (cuspTranslationQuotientMap w hw)

The descended q-parameter is a homeomorphism.

noncomputable def TauCeti.UpperHalfPlane.cuspTranslationQuotientHomeomorph (w : ℝ) (hw : 0 < w) : CuspTranslationQuotient w ≃ₜ { q : Complex.UnitDisc // q ≠ 0 }

The q-parameter identifies the width-translation quotient of the upper half-plane homeomorphically with the punctured unit disc.

Equations

• TauCeti.UpperHalfPlane.cuspTranslationQuotientHomeomorph w hw = IsHomeomorph.homeomorph (TauCeti.UpperHalfPlane.cuspTranslationQuotientMap w hw) ⋯

@[simp]

theorem TauCeti.UpperHalfPlane.cuspTranslationQuotientHomeomorph_mk (w : ℝ) (hw : 0 < w) (z : UpperHalfPlane) : (cuspTranslationQuotientHomeomorph w hw) (Quotient.mk'' z) = qParamPuncturedUnitDisc w hw z

@[simp]

theorem TauCeti.UpperHalfPlane.cuspTranslationQuotientHomeomorph_symm_apply (w : ℝ) (hw : 0 < w) (q : { q : Complex.UnitDisc // q ≠ 0 }) : (cuspTranslationQuotientHomeomorph w hw).symm q = Quotient.mk'' (invQParamUpperHalfPlane w hw q)