Source indexedtheorem · leanprover/lean4:v4.32.0

FKS2.FloorButhe.floor_buthe_of_curve

PrimeNumberTheoremAnd.IEANTN.FKS2Cor23 · PrimeNumberTheoremAnd/IEANTN/FKS2Cor23.lean:472 to 495

Source documentation

Generic Buthe floor assembler: any curve rE whose dyadic slab check passes (hchk) and which dominates the admissible curve on [e^5, e^10] (hcurve) gives Eπ ≤ that curve there. The Buthe Eπ-upper-bound (lhsE, Epi_le_evalLhsE) and the slab cover (slabs, cover) are curve-independent and reused by every row. Bottoms out only at Buthe theorem_2e/2f + li.two_approx.

Exact Lean statement

theorem floor_buthe_of_curve (rE : Expr) (A B C : ℝ)
    (hchk : checkExprLeOnSlabsDyadic lhsE rE slabs (-50) 6 = true)
    (hcurve : ∀ x, (5:ℝ) ≤ Real.log x →
        Expr.eval (fun _ => Real.sqrt (Real.log x)) rE ≤ admissible_bound A B C 5.5666305 x) :
    ∀ x ∈ Set.Icc (Real.exp 5) (Real.exp 10),
      Eπ x ≤ admissible_bound A B C 5.5666305 x

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem floor_buthe_of_curve (rE : Expr) (A B C : ℝ)    (hchk : checkExprLeOnSlabsDyadic lhsE rE slabs (-50) 6 = true)    (hcurve : ∀ x, (5:ℝ) ≤ Real.log x →        Expr.eval (fun _ => Real.sqrt (Real.log x)) rE ≤ admissible_bound A B C 5.5666305 x) :    ∀ x ∈ Set.Icc (Real.exp 5) (Real.exp 10),      Eπ x ≤ admissible_bound A B C 5.5666305 x := by  intro x hx  obtain ⟨h5, h10⟩ := hx  have hxpos : (0:ℝ) < x := lt_of_lt_of_le (Real.exp_pos _) h5  have hLge5 : (5:ℝ) ≤ Real.log x := by    rw [← Real.log_exp 5]; exact Real.log_le_log (Real.exp_pos _) h5  have hLle10 : Real.log x ≤ 10 := by    rw [← Real.log_exp 10]; exact Real.log_le_log hxpos h10  have hs_mem : Real.sqrt (Real.log x) ∈ Set.Icc (2.236 : ℝ) 3.163 := by    constructor    · rw [show (2.236:ℝ) = Real.sqrt (2.236^2) from (Real.sqrt_sq (by norm_num)).symm]      exact Real.sqrt_le_sqrt (by nlinarith [hLge5])    · rw [show (3.163:ℝ) = Real.sqrt (3.163^2) from (Real.sqrt_sq (by norm_num)).symm]      exact Real.sqrt_le_sqrt (by nlinarith [hLle10])  obtain ⟨I, hI, hmem⟩ := cover _ hs_mem  calc Eπ x ≤ Expr.eval (fun _ => Real.sqrt (Real.log x)) lhsE := Epi_le_evalLhsE x h5 h10    _ ≤ Expr.eval (fun _ => Real.sqrt (Real.log x)) rE :=        verify_expr_le_on_slabs_dyadic lhsE rE slabs (-50) 6 (by norm_num) hchk I hI _ hmem    _ ≤ admissible_bound A B C 5.5666305 x := hcurve x hLge5