OAI/NumberTheory/TwoPoint/Halasz/HalaszHurwitzTail.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TwoPointCorrelations.halasz_hurwitz_difference_tail line 12
2. theorem OAI.TwoPointCorrelations.halasz_hurwitz_cutoff_transfer line 42

   Source documentation

   Transfer any unshifted zeta truncation bound to a uniform Hurwitz truncation bound. The additional error has the same decay as Euler's first-order remainder.

   theorem halasz_hurwitz_cutoff_transfer {a : ℝ} (ha : a∈Set.Icc (0:ℝ) 1)
       {s : ℂ} (hs : 0<s.re) {N : ℕ} (hN : 1≤N) {E : ℝ}
       (hE : ‖riemannZeta s-(∑ n∈range N,((n+1:ℕ):ℂ)^(-s))‖≤E) :
       ‖hurwitzZeta (a:UnitAddCircle) s-mrtHurwitzFirstTerm a s-
         (∑ n∈range N,(((n+1:ℕ):ℝ)+a:ℂ)^(-s))‖≤
         E+‖s‖*(N:ℝ)^(-s.re)/s.re := by
   …

   Mentions: OAI.TwoPointCorrelations.mrtHurwitzFirstTerm