Source indexedtheorem · leanprover/lean4:v4.32.0

FKS2.floor_buthe_of_curve_gen

PrimeNumberTheoremAnd.IEANTN.FKS2Cor23 · PrimeNumberTheoremAnd/IEANTN/FKS2Cor23.lean:508 to 535

Source documentation

Generalized Buthe floor assembler: like FloorButhe.floor_buthe_of_curve but with an arbitrary split point xlo ≥ 5 and slab list slabsFrom slabLo n, so the slab interval can start above √5 for rows whose curve the Buthe bound only clears higher up (e.g. row 3 at √6). xlo ≥ 5 keeps Epi_le_evalLhsE applicable.

Exact Lean statement

theorem floor_buthe_of_curve_gen (rE : Expr) (A B C : ℝ) (xlo : ℝ) (slabLo : ℚ) (n : ℕ)
    (hxlo : (5:ℝ) ≤ xlo)
    (hslo : (slabLo:ℝ) ≤ Real.sqrt xlo)
    (hshi : Real.sqrt 10 < (slabLo:ℝ) + (n:ℝ) * 0.05)
    (hchk : checkExprLeOnSlabsDyadic FloorButhe.lhsE rE (slabsFrom slabLo n) (-50) 6 = true)
    (hcurve : ∀ x, xlo ≤ 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 xlo) (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_gen (rE : Expr) (A B C : ℝ) (xlo : ℝ) (slabLo : ℚ) (n : ℕ)    (hxlo : (5:ℝ) ≤ xlo)    (hslo : (slabLo:ℝ) ≤ Real.sqrt xlo)    (hshi : Real.sqrt 10 < (slabLo:ℝ) + (n:ℝ) * 0.05)    (hchk : checkExprLeOnSlabsDyadic FloorButhe.lhsE rE (slabsFrom slabLo n) (-50) 6 = true)    (hcurve : ∀ x, xlo ≤ 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 xlo) (Real.exp 10),      Eπ x ≤ admissible_bound A B C 5.5666305 x := by  intro x hx  obtain ⟨hlo, h10⟩ := hx  have h5 : Real.exp 5 ≤ x := le_trans (Real.exp_le_exp.mpr hxlo) hlo  have hxpos : (0:ℝ) < x := lt_of_lt_of_le (Real.exp_pos _) h5  have hLgexlo : xlo ≤ Real.log x := by    rw [← Real.log_exp xlo]; exact Real.log_le_log (Real.exp_pos _) hlo  have hLle10 : Real.log x ≤ 10 := by    rw [← Real.log_exp 10]; exact Real.log_le_log hxpos h10  have hcov_lo : (slabLo:ℝ) ≤ Real.sqrt (Real.log x) :=    le_trans hslo (Real.sqrt_le_sqrt hLgexlo)  have hcov_hi : Real.sqrt (Real.log x) < (slabLo:ℝ) + (n:ℝ) * 0.05 :=    lt_of_le_of_lt (Real.sqrt_le_sqrt hLle10) hshi  obtain ⟨I, hI, hmem⟩ := coverFrom slabLo n _ hcov_lo hcov_hi  calc Eπ x ≤ Expr.eval (fun _ => Real.sqrt (Real.log x)) FloorButhe.lhsE :=        FloorButhe.Epi_le_evalLhsE x h5 h10    _ ≤ Expr.eval (fun _ => Real.sqrt (Real.log x)) rE :=        verify_expr_le_on_slabs_dyadic FloorButhe.lhsE rE (slabsFrom slabLo n) (-50) 6          (by norm_num) hchk I hI _ hmem    _ ≤ admissible_bound A B C 5.5666305 x := hcurve x hLgexlo