Source indexedtheorem · leanprover/lean4:v4.32.0

Kadiri.zetaCountingDyadic_abs_N_le_backlund_majorant

PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting · PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.lean:834 to 844

Source documentation

An RvM estimate with Backlund's constants gives the dyadic N(T) bound by the explicit majorant.

Exact Lean statement

theorem zetaCountingDyadic_abs_N_le_backlund_majorant
    (hRvM : riemannZeta.Riemann_vonMangoldt_bound 0.137 0.443 6.1) (k : ℕ) :
    |riemannZeta.N ((2 : ℝ) ^ (k + 1))| ≤
      zetaCountingDyadicMajorant 0.137 0.443 6.1 k

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem zetaCountingDyadic_abs_N_le_backlund_majorant    (hRvM : riemannZeta.Riemann_vonMangoldt_bound 0.137 0.443 6.1) (k : ℕ) :    |riemannZeta.N ((2 : ℝ) ^ (k + 1))| ≤      zetaCountingDyadicMajorant 0.137 0.443 6.1 k := by  have hk : (1 : ℕ) ≤ k + 1 := by omega  have hT : (2 : ℝ) ≤ (2 : ℝ) ^ (k + 1) := by    have hpow : (2 : ℝ) ^ (1 : ℕ) ≤ (2 : ℝ) ^ (k + 1) :=      pow_le_pow_right₀ (by norm_num : (1 : ℝ) ≤ 2) (by exact_mod_cast hk)    norm_num at hpow    exact hpow  exact zetaCounting_abs_N_le_backlund_majorant hRvM hT