MRTZetaPole.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Uniform removal of the zeta pole on a bounded part of the closed right half-plane.

def OAI.TwoPointCorrelations.mrtZetaPoleCorrection line 13
lemma OAI.TwoPointCorrelations.mrt_zeta_pole_correction_continuousAt line 16
theorem OAI.TwoPointCorrelations.mrt_zeta_pole_correction_bounded line 26
Source documentation
After subtracting the pole, the logarithmic derivative is uniformly bounded on each bounded part of Re s ≥ 1, with constants independent of characters.
```
theorem mrt_zeta_pole_correction_bounded (B : ℝ) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ s : ℂ, 1 ≤ s.re → ‖s‖ ≤ B → s ≠ 1 →
      ‖mrtZetaPoleCorrection s‖ ≤ C := by
…
```
Mentions: OAI.TwoPointCorrelations.mrtZetaPoleCorrection
lemma OAI.TwoPointCorrelations.mrt_zeta_neg_logderiv_bounded line 56