Source indexedtheorem · leanprover/lean4:v4.32.0

LogDerivZetaUniformLogSquaredBound

PrimeNumberTheoremAnd.StrongPNT · PrimeNumberTheoremAnd/StrongPNT.lean:1807 to 1847

Mathematical statement

Exact Lean statement

@[blueprint
  (title := "LogDerivZetaUniformLogSquaredBound")
  (statement := /--
    There exists a constant $F\in(0,1/2)$ such that for all $t\in\mathbb{R}$ with $|t|\geq 3$ one has
    $$1-\frac{F}{\log|t|}\leq\sigma\implies\left|\frac{\zeta'}{\zeta}(\sigma+it)\right|\ll\log^2|t|$$
    where the implied constant is uniform in $\sigma$.
  -/)
  (proof := /--
    Note that
    $$\left|\frac{\zeta'}{\zeta}(\sigma+it)\right|
      =\sum_{1\leq n}\frac{\Lambda(n)}{|n^{\sigma+it}|}=\sum_{1\leq n}\frac{\Lambda(n)}{n^\sigma}
      =-\frac{\zeta'}{\zeta}(\sigma)\leq\left|\frac{\zeta'}{\zeta}(\sigma)\right|.$$
    From Theorem \ref{riemannZetaLogDerivResidue}, and applying the triangle inequality we know that
    $$\left|\frac{\zeta'}{\zeta}(s)\right|\leq\frac{1}{|s-1|}+C.$$
    where $C>0$ is some constant. Thus, for $\sigma\geq 3/2$ we have that
    $$\left|\frac{\zeta'}{\zeta}(\sigma+it)\right|
      \leq\left|\frac{\zeta'}{\zeta}(\sigma)\right|
      \leq\frac{1}{\sigma-1}+C\leq 2+C\ll 1\ll\log^2|t|.$$
    Putting this together with Lemma \ref{LogDerivZetaUniformLogSquaredBoundStrip}
    completes the proof.
  -/)
  (proofUses := ["riemannZetaLogDerivResidue", "LogDerivZetaUniformLogSquaredBoundStrip"])
  (latexEnv := "theorem")]
theorem LogDerivZetaUniformLogSquaredBound : ∃ (C : ℝ) (_Cnonneg : 0 ≤ C),
    ∀ (σ t : ℝ), 3 < |t| → σ ∈ Set.Ici (1 - F / Real.log |t|) →
      ‖ζ' (σ + t * I) / ζ (σ + t * I)‖ ≤ C * Real.log |t| ^ 2

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

@[blueprint  (title := "LogDerivZetaUniformLogSquaredBound")  (statement := /--    There exists a constant $F\in(0,1/2)$ such that for all $t\in\mathbb{R}$ with $|t|\geq 3$ one has    $$1-\frac{F}{\log|t|}\leq\sigma\implies\left|\frac{\zeta'}{\zeta}(\sigma+it)\right|\ll\log^2|t|$$    where the implied constant is uniform in $\sigma$.  -/)  (proof := /--    Note that    $$\left|\frac{\zeta'}{\zeta}(\sigma+it)\right|      =\sum_{1\leq n}\frac{\Lambda(n)}{|n^{\sigma+it}|}=\sum_{1\leq n}\frac{\Lambda(n)}{n^\sigma}      =-\frac{\zeta'}{\zeta}(\sigma)\leq\left|\frac{\zeta'}{\zeta}(\sigma)\right|.$$    From Theorem \ref{riemannZetaLogDerivResidue}, and applying the triangle inequality we know that    $$\left|\frac{\zeta'}{\zeta}(s)\right|\leq\frac{1}{|s-1|}+C.$$    where $C>0$ is some constant. Thus, for $\sigma\geq 3/2$ we have that    $$\left|\frac{\zeta'}{\zeta}(\sigma+it)\right|      \leq\left|\frac{\zeta'}{\zeta}(\sigma)\right|      \leq\frac{1}{\sigma-1}+C\leq 2+C\ll 1\ll\log^2|t|.$$    Putting this together with Lemma \ref{LogDerivZetaUniformLogSquaredBoundStrip}    completes the proof.  -/)  (proofUses := ["riemannZetaLogDerivResidue", "LogDerivZetaUniformLogSquaredBoundStrip"])  (latexEnv := "theorem")]theorem LogDerivZetaUniformLogSquaredBound : ∃ (C : ℝ) (_Cnonneg : 0 ≤ C),    ∀ (σ t : ℝ), 3 < |t| → σ ∈ Set.Ici (1 - F / Real.log |t|) →      ‖ζ' (σ + t * I) / ζ (σ + t * I)‖ ≤ C * Real.log |t| ^ 2 := by  obtain ⟨C1, hC1⟩ := LogDerivZetaUniformLogSquaredBoundStripSpec  obtain ⟨C2, hC2⟩ := LogDerivZetaBdd_of_Re_ge_three_halves  use max C1 C2, le_max_of_le_left hC1.1  intro σ t ht hσ  by_cases hσ' : σ ≤ 3 / 2  · exact (hC1.2 σ t (by grind) ⟨hσ, hσ'⟩).trans      (mul_le_mul_of_nonneg_right (le_max_left _ _) (sq_nonneg _))  · refine (hC2 _ ?_).trans ?_    · norm_num; linarith    · have hC2pos := (norm_nonneg _).trans (hC2 2 (by norm_num))      exact (le_max_right _ _).trans (le_mul_of_one_le_right        (le_max_of_le_right (by grind))        (one_le_pow₀ (by          rw [Real.le_log_iff_exp_le (by grind)]          exact Real.exp_one_lt_d9.le.trans (by grind))))