Source indexedlemma · leanprover/lean4:v4.32.0

FKS2.admissible_quarter_eq

PrimeNumberTheoremAnd.IEANTN.FKS2Cor23 · PrimeNumberTheoremAnd/IEANTN/FKS2Cor23.lean:541 to 555

Source documentation

admissible_bound A (1/4) C R x in terms of s = √(log x): = (A/R^{1/4})·√s·exp(−(C/√R)·s). (√s = (log x)^{1/4}.)

Exact Lean statement

lemma admissible_quarter_eq (A C R x : ℝ) (hL : 0 ≤ Real.log x) (hR : 0 < R) :
    admissible_bound A 0.25 C R x
      = (A / R ^ ((1:ℝ)/4)) * Real.sqrt (Real.sqrt (Real.log x))
        * Real.exp (-(C / Real.sqrt R) * Real.sqrt (Real.log x))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma admissible_quarter_eq (A C R x : ℝ) (hL : 0 ≤ Real.log x) (hR : 0 < R) :    admissible_bound A 0.25 C R x      = (A / R ^ ((1:ℝ)/4)) * Real.sqrt (Real.sqrt (Real.log x))        * Real.exp (-(C / Real.sqrt R) * Real.sqrt (Real.log x)) := by  set s := Real.sqrt (Real.log x) with hs_def  have hs_rpow : s = Real.log x ^ ((1:ℝ)/2) := by rw [hs_def, Real.sqrt_eq_rpow]  have hsqrts : Real.sqrt s = Real.log x ^ ((1:ℝ)/4) := by    rw [hs_def, Real.sqrt_eq_rpow, Real.sqrt_eq_rpow, ← Real.rpow_mul hL]; norm_num  unfold admissible_bound  have e1 : (Real.log x / R) ^ (0.25:ℝ) = Real.sqrt s / R ^ ((1:ℝ)/4) := by    rw [show (0.25:ℝ) = (1:ℝ)/4 by norm_num, Real.div_rpow hL hR.le, ← hsqrts]  have e2 : (Real.log x / R) ^ ((1:ℝ)/2) = s / Real.sqrt R := by    rw [Real.div_rpow hL hR.le, Real.sqrt_eq_rpow R, ← hs_rpow]  rw [e1, e2, show -C * (s / Real.sqrt R) = -(C / Real.sqrt R) * s by ring]  ring