Source indexedtheorem · leanprover/lean4:v4.32.0

FKS2.psi_le_bound_large

PrimeNumberTheoremAnd.IEANTN.FKS2 · PrimeNumberTheoremAnd/IEANTN/FKS2.lean:2537 to 2554

Source documentation

Bound for ψ(y) for large y.

Exact Lean statement

theorem psi_le_bound_large (y : ℝ) (hy : 1e19 < y) :
    ψ y ≤ 1.00000002 * y + 0.94 * y ^ (1/2 : ℝ)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem psi_le_bound_large (y : ℝ) (hy : 1e19 < y) :    ψ y ≤ 1.00000002 * y + 0.94 * y ^ (1/2 : ℝ) := by  have h_b : |ψ y - y| ≤ BKLNW_app.table_8_ε (19 * log 10) * y := by    apply BKLNW_app.theorem_2 (19 * log 10) (by positivity) y (by      rw [mul_comm, exp_mul, exp_log (by positivity)]; linarith)  have h_eps : BKLNW_app.table_8_ε (19 * log 10) ≤ 1.93378e-8 * BKLNW_app.table_8_margin := by    have h_log_approx : 43 < 19 * log 10 ∧ 19 * log 10 < 44 :=      ⟨by nlinarith [LogTables.log_10_gt], by nlinarith [LogTables.log_10_lt]⟩    grw [BKLNW_app.table_8_ε.le_simp (19 * log 10) (by grind)]    norm_num [BKLNW_app.table_8_ε', h_log_approx]; norm_num at *    field_simp    rw [if_neg (by linarith), if_neg (by linarith), if_neg (by linarith),        if_neg (by linarith), if_neg (by linarith), if_neg (by linarith),        if_neg (by linarith), if_neg (by linarith), if_neg (by linarith),        if_pos (by linarith)]    norm_num [log_pos] at *  norm_num [← sqrt_eq_rpow] at *  nlinarith [abs_le.mp h_b, sqrt_nonneg y, sq_sqrt (show 0 ≤ y by linarith), h_eps]