PV Chain Assembly: Residue Side #
The residue side of the PV chain assembly, showing that the ε-truncated
integral of f'/f around fdBoundaryH H tends to 2πi · Σ gWN · ord.
Main Results #
cpv_residue_side_tendsto— the ε-truncated integral tends to2πi · Σ gWN · ord
Residue side #
theorem
cpv_residue_side_tendsto
{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 →
Filter.Tendsto (fun (ε : ℝ) => ∫ (t : ℝ) in 0..5, pvIntegrand f (fdBoundaryH H) (sArcOfS S ∪ sVertOfS S) ε t)
(nhdsWithin 0 (Set.Ioi 0))
(nhds
(2 * ↑Real.pi * Complex.I * ∑ s ∈ S, generalizedWindingNumber' (fdBoundaryH H) 0 5 ↑s * ↑(orderOfVanishingAt' (⇑f) s)))
Residue side: ε-truncated integral of f'/f tends to 2πi · Σ gWN · ord.