Source indexedtheorem · leanprover/lean4:v4.32.0

Kadiri.zetaCountingRvM_dyadic_le

PrimeNumberTheoremAnd.IEANTN.KadiriZeroCounting · PrimeNumberTheoremAnd/IEANTN/KadiriZeroCounting.lean:995 to 1009

Source documentation

The RvM error term has the dyadic growth needed by the zero-tail route.

Exact Lean statement

theorem zetaCountingRvM_dyadic_le (k : ℕ) :
    riemannZeta.RvM 0.137 0.443 6.1 ((2 : ℝ) ^ (k + 1)) ≤
      7 * ((k + 1 : ℕ) : ℝ) * ((2 : ℝ) ^ k)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem zetaCountingRvM_dyadic_le (k : ℕ) :    riemannZeta.RvM 0.137 0.443 6.1 ((2 : ℝ) ^ (k + 1)) ≤      7 * ((k + 1 : ℕ) : ℝ) * ((2 : ℝ) ^ k) := by  let target : ℝ := ((k + 1 : ℕ) : ℝ) * ((2 : ℝ) ^ k)  have htarget_ge_one : (1 : ℝ) ≤ target := dyadicCountScale_ge_one k  have hlog_le : Real.log ((2 : ℝ) ^ (k + 1)) ≤ target :=    log_dyadic_le_count_scale k  have hTge1 : (1 : ℝ) ≤ (2 : ℝ) ^ (k + 1) :=    one_le_pow₀ (by norm_num : (1 : ℝ) ≤ 2)  have hlog_nonneg : 0 ≤ Real.log ((2 : ℝ) ^ (k + 1)) :=    Real.log_nonneg hTge1  have hloglog_le : Real.log (Real.log ((2 : ℝ) ^ (k + 1))) ≤ target := by    exact (Real.log_le_self hlog_nonneg).trans hlog_le  unfold riemannZeta.RvM  nlinarith