Source indexedlemma · leanprover/lean4:v4.32.0

FKS2.admissible_two_eq

PrimeNumberTheoremAnd.IEANTN.FKS2Cor23Row9 · PrimeNumberTheoremAnd/IEANTN/FKS2Cor23Row9.lean:24 to 39

Source documentation

admissible_bound A 2 C R x in terms of s = √(log x): = (A/R²)·s⁴·exp(−(C/√R)·s). The B = 2 analogue of admissible_three_halves_eq.

Exact Lean statement

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

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma admissible_two_eq (A C R x : ℝ) (hL : 0 ≤ Real.log x) (hR : 0 < R) :    admissible_bound A 2 C R x      = (A / R ^ (2:ℝ)) * Real.sqrt (Real.log x) ^ 4        * 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) ^ (2:ℝ) = s ^ 4 / R ^ (2:ℝ) := by    rw [Real.div_rpow hL hR.le]    congr 1    rw [hs, ← Real.rpow_natCast (Real.log x ^ ((1:ℝ)/2)) 4, ← 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