Source indexedtheorem · leanprover/lean4:v4.32.0

Backlund.zetaCounting_crude_majorant

PrimeNumberTheoremAnd.Backlund.ZeroCountCrude · PrimeNumberTheoremAnd/Backlund/ZeroCountCrude.lean:1101 to 1115

Source documentation

A crude polynomial majorant for the zero-counting function riemannZeta.N, unconditional and with no argument-principle input. The constant is existential (the growth and ball-count inputs are existential); the intended consumer, dyadic summability over the zeta zeros, is indifferent to its value.

Exact Lean statement

theorem zetaCounting_crude_majorant :
    ∃ A : ℝ, 0 < A ∧ ∀ T : ℝ, 2 ≤ T →
      |riemannZeta.N T| ≤ A * T ^ (3/2 : ℝ)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem zetaCounting_crude_majorant :    ∃ A : ℝ, 0 < A ∧ ∀ T : ℝ, 2 ≤ T →      |riemannZeta.N T| ≤ A * T ^ (3/2 : ℝ) := by  obtain ⟨C', hC'0, hC'⟩ := zetaSurrogate_zeros_in_closedBall₀_count  refine ⟨C' * 4 ^ (3/2 : ℝ), mul_pos hC'0 (Real.rpow_pos_of_pos (by norm_num) _), ?_⟩  intro T hT  have h12 : |riemannZeta.N T| ≤ C' * (1 + (T + 1)) ^ (3/2 : ℝ) :=    (zetaCounting_le_surrogate_mass T hT).trans (hC' (T + 1) (by linarith))  have h3 : (1 + (T + 1) : ℝ) ^ (3/2 : ℝ) ≤ 4 ^ (3/2 : ℝ) * T ^ (3/2 : ℝ) := by    rw [← Real.mul_rpow (by norm_num) (by linarith : (0 : ℝ) ≤ T)]    exact Real.rpow_le_rpow (by linarith) (by linarith) (by norm_num)  calc |riemannZeta.N T|      ≤ C' * (1 + (T + 1)) ^ (3/2 : ℝ) := h12    _ ≤ C' * (4 ^ (3/2 : ℝ) * T ^ (3/2 : ℝ)) := mul_le_mul_of_nonneg_left h3 hC'0.le    _ = C' * 4 ^ (3/2 : ℝ) * T ^ (3/2 : ℝ) := by ring