Source indexedlemma · leanprover/lean4:v4.32.0

FKS2.admissible_half_eq

PrimeNumberTheoremAnd.IEANTN.FKS2Cor23 · PrimeNumberTheoremAnd/IEANTN/FKS2Cor23.lean:132 to 144

Source documentation

admissible_bound A (1/2) C R x in terms of s = √(log x): = (A/√R)·s·exp(−(C/√R)·s). The B = 1/2 analogue of admissible_three_halves_eq (used by row 3).

Exact Lean statement

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