Seg5 Cusp Integral

This file contains the cusp-function infrastructure needed to prove that the horizontal edge integral (seg5) of logDeriv(f) equals 2πi · orderAtCusp'(f).

The argument proceeds in two stages:

Stage 1 (seg5_integral_eq_circleIntegral_H): Change of variables from the parametric integral along seg5 to a circle integral in the q-plane.

Stage 2 (circleIntegral_logDeriv_cuspFunction_of_radius): Compute the circle integral using the factorization F(q) = q^m · g(q):

• ∮ m/q dq = m · 2πi from circleIntegral_const_mul_inv
• ∮ logDeriv(g) dq = 0 from circleIntegral_logDeriv_regular_zero

Main Results

• seg5_logDeriv_integral_eq_H — the logDeriv integral along seg5 at height H equals 2πi · orderAtCusp' f.
• seg5_logDeriv_integral_value_bridge — bridge to the form used in PVChain.Assembly.

Cusp function factorization helpers

Circle integral helpers

q-radius positivity

theorem seg5_q_radius_H_pos (H : ℝ) : 0 < seg5QRadiusH H

seg5QRadiusH H > 0 for any H.

Circle integral of logDeriv(cuspFunction)

theorem circleIntegral_logDeriv_cuspFunction_of_radius {k : ℤ} (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) (hf : f ≠ 0) {R : ℝ} (hR_pos : 0 < R) (hR_lt : R < 1) (hcusp_nonvan : ∀ q ∈ Metric.closedBall 0 R, q ≠ 0 → UpperHalfPlane.cuspFunction 1 (⇑f) q ≠ 0) : ∮ (q : ℂ) in C(0, R), logDeriv (UpperHalfPlane.cuspFunction 1 ⇑f) q = 2 * ↑Real.pi * Complex.I * ↑(orderAtCusp' f)

Circle integral of logDeriv(cuspFunction) at any radius 0 < R < 1.

This is the radius-parameterized version. The factorization F(q) = q^m · g(q) gives: ∮ logDeriv(F) = m · ∮ 1/q + ∮ logDeriv(g) = m · 2πi + 0.

Height-Parameterized Seg5 Helpers

theorem seg5_integral_eq_circleIntegral_H {k : ℤ} (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) {H : ℝ} (hH : 0 < H) : ∫ (t : ℝ) in 4..5, logDeriv (modularFormCompOfComplex f) (fdBoundarySeg5H H t) = ∮ (q : ℂ) in C(0, seg5QRadiusH H), logDeriv (UpperHalfPlane.cuspFunction 1 ⇑f) q

Stage 1 (H): The parametric integral of logDeriv(f) along seg5 at height H equals the circle integral of logDeriv(cuspFunction) at radius seg5QRadiusH H.

theorem seg5_logDeriv_integral_eq_H {k : ℤ} (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) (hf : f ≠ 0) {H : ℝ} (hH : 0 < H) (hcusp_nonvan : ∀ q ∈ Metric.closedBall 0 (seg5QRadiusH H), q ≠ 0 → UpperHalfPlane.cuspFunction 1 (⇑f) q ≠ 0) : ∫ (t : ℝ) in 4..5, logDeriv (modularFormCompOfComplex f) (fdBoundarySeg5H H t) = 2 * ↑Real.pi * Complex.I * ↑(orderAtCusp' f)

Combination of Stages 1 and 2 at height H: the logDeriv integral along seg5 at height H = 2πi · orderAtCusp'.

Bridge lemma for Assembly.lean

theorem seg5_logDeriv_integral_value_bridge {k : ℤ} (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) (hf : f ≠ 0) {H : ℝ} (hH : √3 / 2 < H) (hcusp_nonvan : ∀ q ∈ Metric.closedBall 0 (seg5QRadiusH H), q ≠ 0 → UpperHalfPlane.cuspFunction 1 (⇑f) q ≠ 0) : ∫ (t : ℝ) in 4..5, logDeriv (modularFormCompOfComplex f) (fdBoundaryH H t) * deriv (fdBoundaryH H) t = 2 * ↑Real.pi * Complex.I * ↑(orderAtCusp' f)

Bridge lemma: the logDeriv integral along seg5 (with deriv (fdBoundaryH H) t) equals 2πi · orderAtCusp' f.

This connects seg5_logDeriv_integral_eq_H (which integrates just logDeriv f(z(t))) to the form used in PVChain.Assembly, which integrates logDeriv f(z(t)) * z'(t).

For t > 4, fdBoundaryH H t = fdBoundarySeg5H H t and deriv (fdBoundaryH H) t = 1, so the integrand with * deriv ... equals the integrand without.