Source indexedtheorem · leanprover/lean4:v4.32.0

FKS2.Table4Ext.Epi_le_evalLhsE_wide

PrimeNumberTheoremAnd.IEANTN.FKS2Cor24Row4 · PrimeNumberTheoremAnd/IEANTN/FKS2Cor24Row4.lean:48 to 96

Source documentation

Buthe Eπ-upper-bound as eval FloorButhe.lhsE on the WIDE range [2, e^43] (vs Epi_le_evalLhsE_low's [2, e^10]): identical reconciliation, but taking the x ≤ 10^19 hypothesis directly (e^43 ≈ 4.7e18 < 10^19), which extends the Buthe reread to the full x^{-1/2}-floor range. Curve-independent, so reusable by every x^{-1/2} row (rows 1–5). Bottoms out at Buthe theorem_2e/2f + li.two_approx.

Exact Lean statement

theorem Epi_le_evalLhsE_wide (x : ℝ) (h2 : (2 : ℝ) ≤ x) (h19 : x ≤ (10 : ℝ) ^ 19) :
    Eπ x ≤ Expr.eval (fun _ => Real.sqrt (Real.log x)) FloorButhe.lhsE

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem Epi_le_evalLhsE_wide (x : ℝ) (h2 : (2 : ℝ) ≤ x) (h19 : x ≤ (10 : ℝ) ^ 19) :    Eπ x ≤ Expr.eval (fun _ => Real.sqrt (Real.log x)) FloorButhe.lhsE := by  have hxpos : (0:ℝ) < x := by linarith  have hLpos : (0:ℝ) < Real.log x := Real.log_pos (by linarith)  have hLnn : (0:ℝ) ≤ Real.log x := le_of_lt hLpos  have h2e := Buthe.theorem_2e h2 h19  have h2f := Buthe.theorem_2f h2 h19  have hsub := li.sub_Li x h2  have hli2 := li.two_approx  have hli2_le : li 2 ≤ 1.0452 := hli2.2  have hpiLi : pi x - Li x = li 2 - (li x - pi x) := by linarith [hsub]  have habs : |pi x - Li x| ≤ (li x - pi x) + li 2 := by    rw [hpiLi, abs_le]    constructor <;> linarith [h2f, hli2.1]  have hEpi_eq : Eπ x = |pi x - Li x| * (Real.log x / x) := by    unfold Eπ    rw [div_div_eq_mul_div, mul_div_assoc]  rw [hEpi_eq]  set B := Real.sqrt x / Real.log x * (1.95 + 3.9 / Real.log x + 19.5 / (Real.log x) ^ 2) with hB_def  have hfactor_nn : (0:ℝ) ≤ Real.log x / x := by positivity  have hstep1 : |pi x - Li x| * (Real.log x / x) ≤ (B + 1.0452) * (Real.log x / x) := by    apply mul_le_mul_of_nonneg_right _ hfactor_nn    calc |pi x - Li x| ≤ (li x - pi x) + li 2 := habs      _ ≤ B + 1.0452 := by          apply add_le_add          · rw [hB_def]; exact h2e          · exact hli2_le  refine le_trans hstep1 (le_of_eq ?_)  have hxne : x ≠ 0 := ne_of_gt hxpos  have hLne : Real.log x ≠ 0 := ne_of_gt hLpos  have hxinv : x⁻¹ = Real.exp (-(Real.log x)) := by    rw [Real.exp_neg, Real.exp_log hxpos]  have hsqrtx : Real.sqrt x = Real.exp (Real.log x / 2) := by    rw [← Real.exp_log (Real.sqrt_pos.mpr hxpos), Real.log_sqrt (le_of_lt hxpos)]  set s := Real.sqrt (Real.log x) with hs_def  have hss : s * s = Real.log x := by rw [hs_def]; exact Real.mul_self_sqrt hLnn  rw [FloorButhe.eval_lhsE, hss]  set L := Real.log x with hL_def  have hLx : L / x = L * Real.exp (-L) := by    rw [div_eq_mul_inv, hxinv]  have hsqrtxE2 : Real.sqrt x * Real.exp (-L) = Real.exp (-L / 2) := by    rw [hsqrtx, ← Real.exp_add]; congr 1; ring  rw [hB_def, hLx]  rw [show (Real.sqrt x / L * (1.95 + 3.9 / L + 19.5 / L ^ 2) + 1.0452) * (L * Real.exp (-L))      = (Real.sqrt x * Real.exp (-L)) * (1.95 + 3.9 / L + 19.5 / L ^ 2)        + 1.0452 * (L * Real.exp (-L)) by        field_simp]  rw [hsqrtxE2]  ring