The ceiling of the boundary contour maps to a q-circle

Under the level-one q-parameter 𝕢 1 z = exp (2πiz), the truncation ceiling of the fundamental-domain boundary — the horizontal from -1/2 + H·i to 1/2 + H·i — traces the circle of radius e^{-2πH} about the origin, traversed once counterclockwise. This is the change of variables that turns the ceiling contour integral of the logarithmic derivative of a level-one form into a q-circle integral of its cusp function, whose value is 2πi times the order at the cusp.

Main declarations

• TauCeti.ModularForm.fdBoundaryQRadius: the radius e^{-2πH} of the ceiling's q-circle, with fdBoundaryQRadius_def, _pos, and _lt_one.
• TauCeti.ModularForm.qParam_fdBoundarySegment5: the ceiling parametrizes the q-circle.
• TauCeti.ModularForm.circleIntegral_logDeriv_cuspFunction: the q-circle integral of the cusp function's logarithmic derivative is 2πi times the cusp order.

References

• AINTLIB LeanModularForms — the valence-formula development (ForMathlib/ValenceFormula/PVChain/Seg5CuspIntegral.lean) this file ports onto the current Mathlib pin.

noncomputable def TauCeti.ModularForm.fdBoundaryQRadius (H : ℝ) : ℝ

The radius of the q-image of the truncation ceiling of the boundary contour at height H. Sealed as a definition so the ceiling bridge, the cusp-function circle integral, and the radius bounds all speak about one constant.

Equations

• TauCeti.ModularForm.fdBoundaryQRadius H = Real.exp (-2 * Real.pi * H)

theorem TauCeti.ModularForm.fdBoundaryQRadius_def (H : ℝ) : fdBoundaryQRadius H = Real.exp (-2 * Real.pi * H)

The defining equation of the q-circle radius, in the normal form of Function.Periodic.norm_qParam.

theorem TauCeti.ModularForm.fdBoundaryQRadius_pos (H : ℝ) : 0 < fdBoundaryQRadius H

The q-circle radius is positive.

theorem TauCeti.ModularForm.fdBoundaryQRadius_lt_one {H : ℝ} (hH : 0 < H) : fdBoundaryQRadius H < 1

The q-circle radius is less than one for a positive truncation height.

theorem TauCeti.ModularForm.qParam_fdBoundarySegment5 (H t : ℝ) : Function.Periodic.qParam 1 (fdBoundarySegment5 H t) = circleMap 0 (fdBoundaryQRadius H) (2 * Real.pi * (t - 9 / 2))

Under the level-one q-parameter, the ceiling of the boundary contour traces the q-circle of radius e^{-2πH}: the segment parameter t ∈ [4, 5] becomes the angle 2π(t - 9/2), sweeping [-π, π] once counterclockwise.

theorem TauCeti.ModularForm.circleIntegral_logDeriv_cuspFunction {g : UpperHalfPlane → ℂ} {H : ℝ} (hga : ∀ q ∈ Metric.closedBall 0 (fdBoundaryQRadius H), AnalyticAt ℂ (UpperHalfPlane.cuspFunction 1 g) q) (hgz : ∀ q ∈ Metric.closedBall 0 (fdBoundaryQRadius H), q ≠ 0 → UpperHalfPlane.cuspFunction 1 g q ≠ 0) : circleIntegral (logDeriv (UpperHalfPlane.cuspFunction 1 g)) 0 (fdBoundaryQRadius H) = 2 * ↑Real.pi * Complex.I * ↑(qExpansionOrderAtCusp 1 g)

The q-circle integral of the logarithmic derivative of the cusp function is 2πi times the q-expansion order at the cusp: the cusp function is analytic on the closed q-disc and vanishes there at most at the origin, so the argument principle localizes the order contribution to the origin — the cusp order, which is 0 when the cusp function does not vanish there. The order is finite because a cusp function vanishing identically near 0 would also vanish somewhere on the punctured disc.

theorem TauCeti.ModularForm.exists_threshold_cuspFunction_ne_zero {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {k : ℤ} [ModularFormClass F (Matrix.SpecialLinearGroup.mapGL ℝ).range k] {f : F} (hf : ⇑f ≠ 0) : ∃ (H₀ : ℝ), ∀ (H : ℝ), H₀ ≤ H → ∀ q ∈ Metric.closedBall 0 (fdBoundaryQRadius H), q ≠ 0 → UpperHalfPlane.cuspFunction 1 (⇑f) q ≠ 0

Above a threshold height, the cusp function is nonvanishing on the punctured contour q-disk: cuspFunction_eventually_ne_zero gives non-vanishing on some punctured neighbourhood of 0, while the contour needs it on the disc of radius fdBoundaryQRadius H = exp (-2πH) — that radius shrinks as H grows, so the disc sits inside the neighbourhood exactly above a threshold. The threshold device follows valence_formula_general_S_FM in ForMathlib/ValenceFormula.lean of AINTLIB.

theorem TauCeti.ModularForm.analyticAt_cuspFunction_of_mem_closedBall {F : Type u_1} [FunLike F UpperHalfPlane ℂ] {k : ℤ} [ModularFormClass F (Matrix.SpecialLinearGroup.mapGL ℝ).range k] (f : F) {H : ℝ} (hH : 0 < H) (q : ℂ) : q ∈ Metric.closedBall 0 (fdBoundaryQRadius H) → AnalyticAt ℂ (UpperHalfPlane.cuspFunction 1 ⇑f) q

The cusp function of a level-one modular form is analytic on the closed q-disk of the contour: it is differentiable on the unit ball, and the disk's radius exp (-2πH) stays below 1.