PV Chain Helpers

Definitions for pvIntegralLogDeriv, the singular sets sArcOfS and sVertOfS, and the two core analytical stubs (cpv_modular_side_of_SarcSvert and cpv_residue_side_of_SarcSvert) that are needed to prove pv_modular_side and pv_residue_side.

Main Results

• cpv_modular_side_of_SarcSvert — the CPV integral of f'/f around fdBoundaryH H equals -(2πi · (k/12 - ord_∞(f))).
• cpv_residue_side_of_SarcSvert — the CPV integral of f'/f around fdBoundaryH H equals 2πi · Σ gWN · ord.

noncomputable def pvIntegrand {k : ℤ} (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) (γ : ℝ → ℂ) (S₀ : Finset ℂ) (ε t : ℝ) : ℂ

The ε-truncated integrand for the PV integral of f'/f along γ, with singular set S₀. Zero when γ(t) is within ε of any s ∈ S₀, otherwise logDeriv f (γ t) * γ'(t).

Equations

• pvIntegrand f γ S₀ ε t = cauchyPrincipalValueIntegrandOn S₀ (logDeriv (modularFormCompOfComplex f)) γ ε t

noncomputable def sArcOfS (S : Finset UpperHalfPlane) : Finset ℂ

Arc singular set: unit-circle zeros (and S-transforms) plus ρ, ρ+1.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def sVertOfS (S : Finset UpperHalfPlane) : Finset ℂ

Vertical singular set: re = ±1/2, ‖z‖ > 1 zeros, plus T-shifts.

Equations

• One or more equations did not get rendered due to their size.

def onCurvePVProvider (S : Finset UpperHalfPlane) : Prop

CPV existence at all on-curve singular points of fdBoundaryH H.

Equations

• One or more equations did not get rendered due to their size.

theorem fdBoundary_H_onCurvePVProvider (S : Finset UpperHalfPlane) : onCurvePVProvider S

CPV exists at every on-curve singular point.

theorem sArcOfS_rho_in (S : Finset UpperHalfPlane) : ellipticPointRho ∈ sArcOfS S

theorem sArcOfS_rho_plus_one_in (S : Finset UpperHalfPlane) : ellipticPointRhoPlusOne ∈ sArcOfS S

theorem sArcOfS_unit (S : Finset UpperHalfPlane) (s : ℂ) : s ∈ sArcOfS S → ‖s‖ = 1

theorem sArcOfS_closed (S : Finset UpperHalfPlane) (s : ℂ) : s ∈ sArcOfS S → -1 / s ∈ sArcOfS S

theorem sVertOfS_re (S : Finset UpperHalfPlane) (s : ℂ) : s ∈ sVertOfS S → s.re = 1 / 2 ∨ s.re = -1 / 2

theorem sVertOfS_pair_left (S : Finset UpperHalfPlane) (s : ℂ) : s ∈ sVertOfS S → s.re = 1 / 2 → s - 1 ∈ sVertOfS S

theorem sVertOfS_pair_right (S : Finset UpperHalfPlane) (s : ℂ) : s ∈ sVertOfS S → s.re = -1 / 2 → s + 1 ∈ sVertOfS S

theorem exists_height_bound_S (S : Finset UpperHalfPlane) : ∃ (H₁ : ℝ), √3 / 2 < H₁ ∧ 1 < H₁ ∧ ∀ s ∈ S, (↑s).im < H₁

There exists a height above √3/2 exceeding all points in S.

theorem sVertOfS_im_lt_height_bound {H₁ : ℝ} (S : Finset UpperHalfPlane) (s : ℂ) (hs : s ∈ sVertOfS S) (h_bound : ∀ p ∈ S, (↑p).im < H₁) : s.im < H₁

All elements of sVertOfS S have im < H₁ when all elements of S have im < H₁.

theorem sum_gWN_ord_eq_filter_zeros {k : ℤ} (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) (S : Finset UpperHalfPlane) (g : ℂ → ℂ) : ∑ s ∈ S, g ↑s * ↑(orderOfVanishingAt' (⇑f) s) = ∑ s ∈ S with f s = 0, g ↑s * ↑(orderOfVanishingAt' (⇑f) s)

Summing gWN · ord over all of S equals summing over just zeros.

theorem sArcOfS_im_pos (S : Finset UpperHalfPlane) (s : ℂ) (hs : s ∈ sArcOfS S) : 0 < s.im

All elements of sArcOfS S have positive imaginary part.

theorem sVertOfS_im_pos (S : Finset UpperHalfPlane) (s : ℂ) (hs : s ∈ sVertOfS S) : 0 < s.im

All elements of sVertOfS S have positive imaginary part.

theorem fdBox_of_on_curve (S : Finset UpperHalfPlane) (hS : ∀ p ∈ S, p ∈ ModularGroup.fd) {H M : ℝ} (_hH_sqrt3 : √3 / 2 < H) (hH_lt_M : H < M) (hH_ge1 : 1 ≤ H) (hH_bound : ∀ s ∈ S, (↑s).im < H) (s : ℂ) (hs : s ∈ sArcOfS S ∪ sVertOfS S) : s ∈ fdBox M

On-curve singular points lie inside fdBox M when H < M.