zetaReciprocal_local_factorization

formal source

 609/-- A local meromorphic factorization of `zetaReciprocal` at a hypothetical
 610zero ρ of ζ in the strip. The regular factor `g` is analytic and nonvanishing
 611on a closed disk, extracted from Mathlib's `meromorphicOrderAt_eq_int_iff`. -/
 612theorem zetaReciprocal_local_factorization (ρ : ℂ)
 613    (hρ_ne : ρ ≠ 1)
 614    (m : ℤ)
 615    (hord : meromorphicOrderAt zetaReciprocal ρ = ↑m) :
 616    ∃ w : LocalMeromorphicWitness, w.center = ρ ∧ w.order = m := by
 617  exact local_meromorphic_factorization zetaReciprocal ρ m
 618    (zetaReciprocal_meromorphicAt ρ hρ_ne) hord
 619
 620/-- Construct a `QuantitativeLocalFactorization` from the Euler carrier data
 621at a hypothetical zero ρ. The log-derivative bound `M` is taken from
 622`carrierDerivBound(Re(ρ))`, which dominates the per-prime log-derivative
 623terms by `eulerPrimeLogDerivTermComplex_summable`. -/
 624noncomputable def eulerQuantitativeFactorization (ρ : ℂ)
 625    (hρ_ne : ρ ≠ 1)
 626    (m : ℤ)
 627    (hord : meromorphicOrderAt zetaReciprocal ρ = ↑m)
 628    (hσ : 1/2 < ρ.re) :
 629    QuantitativeLocalFactorization := by
 630  let w := (zetaReciprocal_local_factorization ρ hρ_ne m hord).choose
 631  let M : ℝ := carrierDerivBound ρ.re
 632  let r : ℝ := min w.radius (1 / M)
 633  have hM_pos : 0 < M := carrierDerivBound_pos hσ
 634  have hr_pos : 0 < r := by
 635    dsimp [r]
 636    exact lt_min w.radius_pos (one_div_pos.mpr hM_pos)
 637  refine
 638    { toLocalMeromorphicWitness :=
 639        w.shrinkRadius r hr_pos (by
 640          dsimp [r]
 641          exact min_le_left _ _)
 642      logDerivBound := M