Source indexedtheorem · leanprover/lean4:v4.32.0

eq12_no_border_poles

PrimeNumberTheoremAnd.IEANTN.KadiriEq12Helpers · PrimeNumberTheoremAnd/IEANTN/KadiriEq12Helpers.lean:464 to 479

Source documentation

No poles on the rectangle border (residue-theorem hyp B2/B3): given that ζ is non-zero and the point is ≠ 1 on the entire border, the eq.(12) integrand is analytic there, hence has non-negative order, so the border is disjoint from the pole set.

Exact Lean statement

theorem eq12_no_border_poles {Φ : ℂ → ℂ} {b : ℝ}
    (hΦ : AnalyticOnNhd ℂ Φ {s : ℂ | -(1 + b) < s.re ∧ s.re < b})
    {a T : ℝ} (ha : 0 < a) (hab : a < b)
    (hborder : ∀ s ∈ RectangleBorder ((-a : ℝ) - (T : ℂ) * I) ((1 + a : ℝ) + (T : ℂ) * I),
        riemannZeta s ≠ 0 ∧ s ≠ 1) :
    Disjoint (RectangleBorder ((-a : ℝ) - (T : ℂ) * I) ((1 + a : ℝ) + (T : ℂ) * I))
      {s | meromorphicOrderAt
        (fun s ↦ (-deriv riemannZeta s / riemannZeta s) * Φ (-s)) s < 0}

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem eq12_no_border_poles {Φ : ℂ → ℂ} {b : ℝ}    (hΦ : AnalyticOnNhd ℂ Φ {s : ℂ | -(1 + b) < s.re ∧ s.re < b})    {a T : ℝ} (ha : 0 < a) (hab : a < b)    (hborder : ∀ s ∈ RectangleBorder ((-a : ℝ) - (T : ℂ) * I) ((1 + a : ℝ) + (T : ℂ) * I),        riemannZeta s ≠ 0 ∧ s ≠ 1) :    Disjoint (RectangleBorder ((-a : ℝ) - (T : ℂ) * I) ((1 + a : ℝ) + (T : ℂ) * I))      {s | meromorphicOrderAt        (fun s ↦ (-deriv riemannZeta s / riemannZeta s) * Φ (-s)) s < 0} := by  rw [Set.disjoint_left]  intro s hs_border hs_pole  simp only [Set.mem_setOf_eq] at hs_pole  obtain ⟨hζ_ne, hs1⟩ := hborder s hs_border  have hs_rect : s ∈ Rectangle ((-a : ℝ) - (T : ℂ) * I) ((1 + a : ℝ) + (T : ℂ) * I) :=    rectangleBorder_subset_rectangle _ _ hs_border  exact absurd hs_pole    (not_lt.mpr (eq12_meromorphicOrderAt_nonneg_of_ne hΦ ha hab hs_rect hζ_ne hs1))