Source indexedlemma · leanprover/lean4:v4.32.0

FKS2.admissible_three_halves_eq

PrimeNumberTheoremAnd.IEANTN.FKS2Cor23 · PrimeNumberTheoremAnd/IEANTN/FKS2Cor23.lean:112 to 127

Source documentation

admissible_bound A (3/2) C R x in terms of s = √(log x): = (A / R^{3/2}) · s³ · exp(−(C/√R)·s). Reusable for tail domination.

Exact Lean statement

lemma admissible_three_halves_eq (A C R x : ℝ) (hL : 0 ≤ Real.log x) (hR : 0 < R) :
    admissible_bound A 1.5 C R x
      = (A / R ^ (1.5:ℝ)) * Real.sqrt (Real.log x) ^ 3
        * Real.exp (-(C / Real.sqrt R) * Real.sqrt (Real.log x))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

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