Source indexedlemma · leanprover/lean4:v4.32.0

FKS2.rowcurve_dom_three_halves

PrimeNumberTheoremAnd.IEANTN.FKS2Cor23 · PrimeNumberTheoremAnd/IEANTN/FKS2Cor23.lean:181 to 205

Source documentation

Generic B = 3/2 floor-curve domination: the evaluated dyadic floor curve coeff·s³·exp(−rate·s) (s = √(log x)) is below the row's admissible curve when coeff ≤ A/R^{3/2} and rate ≥ C/√R. Shared by every B = 3/2 row's rhsE_le_rowcurve (rows 5/6/7).

Exact Lean statement

lemma rowcurve_dom_three_halves (A C coeff rate : ℝ) (x : ℝ)
    (hL : (0:ℝ) ≤ Real.log x)
    (hcoeff : coeff ≤ A / (5.5666305:ℝ) ^ (1.5:ℝ))
    (hrate : C / Real.sqrt 5.5666305 ≤ rate)
    (hcoeffnn : 0 ≤ coeff) :
    coeff * (Real.sqrt (Real.log x) * Real.sqrt (Real.log x) * Real.sqrt (Real.log x))
        * Real.exp (-rate * Real.sqrt (Real.log x))
      ≤ admissible_bound A 1.5 C 5.5666305 x

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma rowcurve_dom_three_halves (A C coeff rate : ℝ) (x : ℝ)    (hL : (0:ℝ) ≤ Real.log x)    (hcoeff : coeff ≤ A / (5.5666305:ℝ) ^ (1.5:ℝ))    (hrate : C / Real.sqrt 5.5666305 ≤ rate)    (hcoeffnn : 0 ≤ coeff) :    coeff * (Real.sqrt (Real.log x) * Real.sqrt (Real.log x) * Real.sqrt (Real.log x))        * Real.exp (-rate * Real.sqrt (Real.log x))      ≤ admissible_bound A 1.5 C 5.5666305 x := by  rw [admissible_three_halves_eq A C 5.5666305 x hL (by norm_num)]  set s := Real.sqrt (Real.log x) with hs_def  have hsnn : (0:ℝ) ≤ s := Real.sqrt_nonneg _  have hsss : s * s * s = s ^ 3 := by ring  have hAnn : (0:ℝ) ≤ A / (5.5666305:ℝ) ^ (1.5:ℝ) := le_trans hcoeffnn hcoeff  have hexpRHS : Real.exp (-rate * s) ≤ Real.exp (-(C / Real.sqrt 5.5666305) * s) := by    apply Real.exp_le_exp.mpr    have := mul_le_mul_of_nonneg_right hrate hsnn    simp only [neg_mul]; linarith  have hs3 : (0:ℝ) ≤ s ^ 3 := by positivity  rw [hsss]  calc coeff * s ^ 3 * Real.exp (-rate * s)      = (coeff * Real.exp (-rate * s)) * s ^ 3 := by ring    _ ≤ ((A / (5.5666305:ℝ) ^ (1.5:ℝ)) * Real.exp (-(C / Real.sqrt 5.5666305) * s)) * s ^ 3 :=        mul_le_mul_of_nonneg_right          (mul_le_mul hcoeff hexpRHS (Real.exp_nonneg _) hAnn) hs3    _ = A / (5.5666305:ℝ) ^ (1.5:ℝ) * s ^ 3 * Real.exp (-(C / Real.sqrt 5.5666305) * s) := by ring