Source indexedtheorem · leanprover/lean4:v4.32.0

FKS2.floor_buthe_quarter_of_curve

PrimeNumberTheoremAnd.IEANTN.FKS2Cor23 · PrimeNumberTheoremAnd/IEANTN/FKS2Cor23.lean:637 to 678

Source documentation

Quarter (B=1/4) Buthe floor assembler on [e^xlo, e^10]: the SQUARED slab check lhsE² ≤ rhsE2 plus the squared-curve domination, sqrt taken outside the kernel. Companion of floor_buthe_of_curve_gen for the half-power rows.

Exact Lean statement

theorem floor_buthe_quarter_of_curve (rhsE2 : Expr) (A C : ℝ) (xlo : ℝ) (slabLo : ℚ) (n : ℕ)
    (hApos : 0 < A)
    (hxlo : (5:ℝ) ≤ xlo)
    (hslo : (slabLo:ℝ) ≤ Real.sqrt xlo)
    (hshi : Real.sqrt 10 < (slabLo:ℝ) + (n:ℝ) * 0.05)
    (hchk : checkExprLeOnSlabsDyadic (Expr.mul FloorButhe.lhsE FloorButhe.lhsE) rhsE2
        (slabsFrom slabLo n) (-50) 6 = true)
    (hcurve2 : ∀ x, xlo ≤ Real.log x →
        Expr.eval (fun _ => Real.sqrt (Real.log x)) rhsE2
          ≤ (admissible_bound A 0.25 C 5.5666305 x) ^ 2) :
    ∀ x ∈ Set.Icc (Real.exp xlo) (Real.exp 10),
      Eπ x ≤ admissible_bound A 0.25 C 5.5666305 x

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem floor_buthe_quarter_of_curve (rhsE2 : Expr) (A C : ℝ) (xlo : ℝ) (slabLo : ℚ) (n : ℕ)    (hApos : 0 < A)    (hxlo : (5:ℝ) ≤ xlo)    (hslo : (slabLo:ℝ) ≤ Real.sqrt xlo)    (hshi : Real.sqrt 10 < (slabLo:ℝ) + (n:ℝ) * 0.05)    (hchk : checkExprLeOnSlabsDyadic (Expr.mul FloorButhe.lhsE FloorButhe.lhsE) rhsE2        (slabsFrom slabLo n) (-50) 6 = true)    (hcurve2 : ∀ x, xlo ≤ Real.log x →        Expr.eval (fun _ => Real.sqrt (Real.log x)) rhsE2          ≤ (admissible_bound A 0.25 C 5.5666305 x) ^ 2) :    ∀ x ∈ Set.Icc (Real.exp xlo) (Real.exp 10),      Eπ x ≤ admissible_bound A 0.25 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 hLpos : (0:ℝ) < Real.log x := lt_of_lt_of_le (by linarith) hLgexlo  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  have hslab2 := verify_expr_le_on_slabs_dyadic (Expr.mul FloorButhe.lhsE FloorButhe.lhsE) rhsE2    (slabsFrom slabLo n) (-50) 6 (by norm_num) hchk I hI _ hmem  rw [Expr.eval_mul] at hslab2  set L := Expr.eval (fun _ => Real.sqrt (Real.log x)) FloorButhe.lhsE with hL_def  have hL_nn : (0:ℝ) ≤ L := by    rw [hL_def, FloorButhe.eval_lhsE]; positivity  have hadm_nn : (0:ℝ) ≤ admissible_bound A 0.25 C 5.5666305 x := by    rw [admissible_quarter_eq A C 5.5666305 x hLpos.le (by norm_num)]; positivity  have hsq : L ^ 2 ≤ (admissible_bound A 0.25 C 5.5666305 x) ^ 2 := by    calc L ^ 2 = L * L := sq L      _ ≤ Expr.eval (fun _ => Real.sqrt (Real.log x)) rhsE2 := hslab2      _ ≤ (admissible_bound A 0.25 C 5.5666305 x) ^ 2 := hcurve2 x hLgexlo  have hL_le : L ≤ admissible_bound A 0.25 C 5.5666305 x := by    have := Real.sqrt_le_sqrt hsq    rwa [Real.sqrt_sq hL_nn, Real.sqrt_sq hadm_nn] at this  exact le_trans (FloorButhe.Epi_le_evalLhsE x h5 h10) hL_le