PV Chain: Residue Side and Modular Side #
Bridge theorems connecting the ε-truncated integral of f'/f
to the generalized winding number sum and the modular transformation.
The key identity pv_chain_identity follows by uniqueness of limits:
both sides are limits of the same ε-truncated integral, so they are equal.
theorem
pv_chain_identity
{k : ℤ}
(f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k)
(hf : f ≠ 0)
(S : Finset UpperHalfPlane)
(hS : ∀ p ∈ S, p ∈ ModularGroup.fd)
(hS_complete : ∀ p ∈ ModularGroup.fd, orderOfVanishingAt' (⇑f) p ≠ 0 → p ∈ S)
:
∃ (H₀ : ℝ),
√3 / 2 < H₀ ∧ ∀ {H : ℝ},
H₀ ≤ H →
∑ s ∈ S, generalizedWindingNumber' (fdBoundaryH H) 0 5 ↑s * ↑(orderOfVanishingAt' (⇑f) s) = -(↑k / 12 - ↑(orderAtCusp' f))
The PV chain identity: equate residue and modular sides via
uniqueness of limits, then cancel 2πi.