Residue-Side Infrastructure for the PV Chain

Infrastructure lemmas needed to apply generalizedResidueTheorem' to logDeriv (modularFormCompOfComplex f) on fdBoundaryH H.

Main Results

• hasSimplePoleAt_logDeriv_of_zero' — logDeriv f has HasSimplePoleAt at zeros
• hasSimplePoleAt_logDeriv_at_nonzero — trivial HasSimplePoleAt at non-zeros
• fdBox_isOpen, fdBox_convex — fdBox properties
• fdBoundary_H_mem_fdBox' — curve is inside fdBox
• residueSimplePole_logDeriv_eq_order — residue = order at zeros
• residueSimplePole_logDeriv_eq_zero_at_nonzero — residue = 0 at non-zeros

fdBox properties

theorem fdBox_isOpen (M : ℝ) : IsOpen (fdBox M)

theorem fdBox_convex (M : ℝ) : Convex ℝ (fdBox M)

allZerosInFdBox

noncomputable def allZerosInFdBox {k : ℤ} (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) (hf : f ≠ 0) {M : ℝ} (hM : 1 / 2 < M) : Finset ℂ

The finite set of zeros of the modular form inside the fundamental-domain box.

Equations

• allZerosInFdBox f hf hM = ⋯.toFinset

theorem mem_allZerosInFdBox_iff {k : ℤ} (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) (hf : f ≠ 0) {M : ℝ} (hM : 1 / 2 < M) {z : ℂ} : z ∈ allZerosInFdBox f hf hM ↔ z ∈ fdBox M ∧ modularFormCompOfComplex f z = 0

HasSimplePoleAt for logDeriv at zeros

theorem analyticAt_logDeriv_off_zeros' {k : ℤ} (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) (z : ℂ) (hz : 0 < z.im) (hfz : modularFormCompOfComplex f z ≠ 0) : AnalyticAt ℂ (logDeriv (modularFormCompOfComplex f)) z

theorem hasSimplePoleAt_logDeriv_of_zero_full {k : ℤ} (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) (hf : f ≠ 0) (s : UpperHalfPlane) (hs : f s = 0) : ∃ (n : ℤ) (g : ℂ → ℂ), n > 0 ∧ AnalyticAt ℂ g ↑s ∧ g ↑s ≠ 0 ∧ n = ↑(analyticOrderNatAt (modularFormCompOfComplex f) ↑s) ∧ ∀ᶠ (z : ℂ) in nhds ↑s, z ≠ ↑s → logDeriv (modularFormCompOfComplex f) z = ↑n / (z - ↑s) + logDeriv g z

logDeriv of a modular form has a simple pole at each zero, with the factorization logDeriv F(z) = n/(z-s) + logDeriv g(z) where n is the vanishing order and g is analytic with g(s) ≠ 0.

theorem hasSimplePoleAt_logDeriv_of_zero' {k : ℤ} (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) (hf : f ≠ 0) (s : UpperHalfPlane) (hs : f s = 0) : HasSimplePoleAt (logDeriv (modularFormCompOfComplex f)) ↑s

logDeriv of a modular form has HasSimplePoleAt at each zero.

theorem hasSimplePoleAt_logDeriv_at_nonzero {k : ℤ} (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) (z : ℂ) (hz_im : 0 < z.im) (hz_nz : modularFormCompOfComplex f z ≠ 0) : HasSimplePoleAt (logDeriv (modularFormCompOfComplex f)) z

HasSimplePoleAt of logDeriv at a non-zero point (trivial: c = 0, g = logDeriv f).

theorem hasSimplePoleAt_logDeriv_at_point {k : ℤ} (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) (hf : f ≠ 0) (z : ℂ) (hz_im : 0 < z.im) : HasSimplePoleAt (logDeriv (modularFormCompOfComplex f)) z

HasSimplePoleAt for any point with positive imaginary part.

ContinuousAt of the regular part (for hf_ext)

orderOfVanishingAt' = analyticOrderNatAt

residueSimplePole lemmas

theorem residueSimplePole_logDeriv_eq_order {k : ℤ} (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) (hf : f ≠ 0) (s : UpperHalfPlane) (hs : f s = 0) : residueSimplePole (logDeriv (modularFormCompOfComplex f)) ↑s = ↑(orderOfVanishingAt' (⇑f) s)

At a zero s of f, residueSimplePole(logDeriv f, s) = orderOfVanishingAt'(f, s).

theorem residueSimplePole_logDeriv_eq_zero_at_nonzero {k : ℤ} (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) (z : ℂ) (hz_im : 0 < z.im) (hz_nz : modularFormCompOfComplex f z ≠ 0) : residueSimplePole (logDeriv (modularFormCompOfComplex f)) z = 0

At a non-zero point, residueSimplePole(logDeriv f, z) = 0.

fdBoundaryH ∈ fdBox

theorem fdBoundary_H_mem_fdBox' {H M : ℝ} (hH : 1 ≤ H) (hM : H < M) (t : ℝ) (ht : t ∈ Set.Icc 0 5) : fdBoundaryH H t ∈ fdBox M

For H ≥ 1 and M > H, fdBoundaryH H t ∈ fdBox M for t ∈ [0, 5].

Discrete set separation

theorem finset_discrete (S0 : Finset ℂ) (s : ℂ) : s ∈ ↑S0 → ∃ ε > 0, ∀ s' ∈ ↑S0, s' ≠ s → ε ≤ ‖s' - s‖

CPV existence at off-curve singular points

theorem cpvExists_of_off_curve (γ : ℝ → ℂ) (hγ_cont : Continuous γ) (a b : ℝ) (s c : ℂ) (hab : a ≤ b) (h_off : ∀ t ∈ Set.Icc a b, γ t ≠ s) : CauchyPrincipalValueExists' (fun (z : ℂ) => c / (z - s)) γ a b s

CPV of c/(z - s) exists when the curve avoids s (limit is just the regular integral).

theorem cpvExists_scale (γ : ℝ → ℂ) (a b : ℝ) (s c : ℂ) (h : CauchyPrincipalValueExists' (fun (z : ℂ) => (z - s)⁻¹) γ a b s) : CauchyPrincipalValueExists' (fun (z : ℂ) => c / (z - s)) γ a b s

CPV of c · (z - s)⁻¹ from CPV of (z - s)⁻¹ by scaling.

logDeriv_patched — patched logDeriv for ContinuousAt at zeros

At zeros of f, Lean's div_zero convention makes logDeriv f(z) = 0/0 = 0, but the limit from the punctured neighborhood is g(z) ≠ 0. This breaks the ContinuousAt hypothesis of generalizedResidueTheorem'.

The fix: define logDerivPatched F S0 which equals F away from S0 and equals the regular part g(z) at each z ∈ S0 (from the HasSimplePoleAt decomposition). This makes the ContinuousAt hypothesis hold.

noncomputable def logDerivPatched (F : ℂ → ℂ) (S0 : Finset ℂ) (hsp : ∀ s ∈ S0, HasSimplePoleAt F s) : ℂ → ℂ

The logarithmic derivative of F, patched to a fixed value at the points of S0.

Equations

• logDerivPatched F S0 hsp z = if h : z ∈ S0 then Classical.choose ⋯ z else F z

theorem logDerivPatched_eq_raw_off (F : ℂ → ℂ) (S0 : Finset ℂ) (hsp : ∀ s ∈ S0, HasSimplePoleAt F s) {z : ℂ} (hz : z ∉ S0) : logDerivPatched F S0 hsp z = F z

theorem hasSimplePoleAt_logDerivPatched (F : ℂ → ℂ) (S0 : Finset ℂ) (hsp : ∀ s ∈ S0, HasSimplePoleAt F s) (s : ℂ) (hs : s ∈ S0) : HasSimplePoleAt (logDerivPatched F S0 hsp) s

theorem residue_logDerivPatched_eq_raw (F : ℂ → ℂ) (S0 : Finset ℂ) (hsp : ∀ s ∈ S0, HasSimplePoleAt F s) (s : ℂ) (hs : s ∈ S0) : residueSimplePole (logDerivPatched F S0 hsp) s = residueSimplePole F s

theorem logDerivPatched_hf_ext (F : ℂ → ℂ) (S0 : Finset ℂ) (hsp : ∀ s ∈ S0, HasSimplePoleAt F s) (s : ℂ) : s ∈ S0 → ContinuousAt (fun (z : ℂ) => logDerivPatched F S0 hsp z - residueSimplePole (logDerivPatched F S0 hsp) s / (z - s)) s

The patched logDeriv satisfies ContinuousAt for generalizedResidueTheorem'.

Norm bounds for fdBoundaryH

theorem fdBoundary_H_norm_ge_one {H : ℝ} (hH : 1 ≤ H) (t : ℝ) (ht : t ∈ Set.Icc 0 5) : ‖fdBoundaryH H t‖ ≥ 1

‖fdBoundaryH H t‖ ≥ 1 for t ∈ [0, 5] when H ≥ 1.

theorem off_curve_of_not_in_fd_H {H : ℝ} (hH : 1 ≤ H) (z₀ : ℂ) (hz₀_not_fd : ¬(|z₀.re| ≤ 1 / 2 ∧ ‖z₀‖ ≥ 1)) (t : ℝ) : t ∈ Set.Icc 0 5 → fdBoundaryH H t ≠ z₀

The boundary fdBoundaryH H avoids every point NOT in the closed FD.

theorem ftc_integral_zero_of_closed_slit {γ : ℝ → ℂ} {z₀ ω : ℂ} (hω : ω ≠ 0) (hγ_cont : Continuous γ) (hγ_closed : γ 0 = γ 5) (h_off : ∀ t ∈ Set.Icc 0 5, γ t ≠ z₀) (h_slit : ∀ t ∈ Set.Icc 0 5, ω * (γ t - z₀) ∈ Complex.slitPlane) (hγ_diff : ∀ t ∉ fdBoundaryFullPartition, DifferentiableAt ℝ γ t) (hγ_deriv_cont : ∀ t ∈ Set.Ioo 0 5, t ∉ fdBoundaryFullPartition → ContinuousAt (deriv γ) t) (hγ_deriv_bdd : ∃ (Mγ : ℝ), ∀ t ∈ Set.Icc 0 5, ‖deriv γ t‖ ≤ Mγ) : ∫ (t : ℝ) in 0..5, (γ t - z₀)⁻¹ * deriv γ t = 0

FTC: integral = 0 for a closed curve with slit-plane avoidance.

theorem winding_zero_for_non_fd_point_H_geo {k : ℤ} (f : ModularForm (Subgroup.map (Matrix.SpecialLinearGroup.mapGL ℝ) (CongruenceSubgroup.Gamma 1)) k) (hf : f ≠ 0) (S : Finset UpperHalfPlane) (hS_complete : ∀ p ∈ ModularGroup.fd, orderOfVanishingAt' (⇑f) p ≠ 0 → p ∈ S) {H : ℝ} (hH : 1 ≤ H) (z₀ : ℂ) (hz₀_zero : z₀ ∈ allZerosInFdBox f hf ⋯) (hz₀_not_S : ∀ s ∈ S, ↑s ≠ z₀) : generalizedWindingNumber' (fdBoundaryH H) 0 5 z₀ = 0

Winding number = 0 for points in fdBox but NOT in the fundamental domain.