The boundary contour integral of a level-one logarithmic derivative #
The four boundary pieces assemble: the two verticals cancel by periodicity, the arc
collapses to its weight term, and the ceiling evaluates through the q-circle to the
cusp order — so the whole boundary contour integral of the logarithmic derivative is
2πi · ord_∞ - k·(π/6)·i. Under the (2πi)⁻¹ normalization of the valence contour this
is ord_∞ - k/12.
Main declarations #
TauCeti.ModularForm.intervalIntegral_logDeriv_fdBoundary: the assembled boundary integral.
References #
- AINTLIB
LeanModularForms— the valence-formula development (ForMathlib/ValenceFormula/PVChain/Assembly.lean) this file ports onto the current Mathlib pin.
theorem
TauCeti.ModularForm.intervalIntegral_logDeriv_fdBoundary
{F : Type u_1}
[FunLike F UpperHalfPlane ℂ]
{Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)}
{k : ℤ}
[SlashInvariantFormClass F (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) Γ) k]
(f : F)
(hS : ModularGroup.S ∈ Γ)
{H : ℝ}
(hper : Function.Periodic (⇑f ∘ ↑UpperHalfPlane.ofComplex) 1)
(hd : ∀ t ∈ Set.Ioo 1 2, DifferentiableAt ℂ (⇑f ∘ ↑UpperHalfPlane.ofComplex) (fdBoundary H t))
(hne : ∀ t ∈ Set.Ioo 1 2, (⇑f ∘ ↑UpperHalfPlane.ofComplex) (fdBoundary H t) ≠ 0)
(hga : ∀ q ∈ Metric.closedBall 0 (fdBoundaryQRadius H), AnalyticAt ℂ (UpperHalfPlane.cuspFunction 1 ⇑f) q)
(hgz : ∀ q ∈ Metric.closedBall 0 (fdBoundaryQRadius H), q ≠ 0 → UpperHalfPlane.cuspFunction 1 (⇑f) q ≠ 0)
(hint01 :
IntervalIntegrable
(fun (t : ℝ) => deriv (fdBoundary H) t • logDeriv (⇑f ∘ ↑UpperHalfPlane.ofComplex) (fdBoundary H t))
MeasureTheory.volume 0 1)
(hint12 :
IntervalIntegrable
(fun (t : ℝ) => deriv (fdBoundary H) t • logDeriv (⇑f ∘ ↑UpperHalfPlane.ofComplex) (fdBoundary H t))
MeasureTheory.volume 1 2)
(hint45 :
IntervalIntegrable
(fun (t : ℝ) => deriv (fdBoundary H) t • logDeriv (⇑f ∘ ↑UpperHalfPlane.ofComplex) (fdBoundary H t))
MeasureTheory.volume 4 5)
:
The boundary contour integral of a level-one logarithmic derivative: the
verticals cancel by periodicity, the arc collapses to its weight term, and the ceiling
evaluates to the cusp order, so the whole contour integral is
2πi · ord_∞ - k·(π/6)·i.