Source indexedlemma · leanprover/lean4:v4.32.0

FKS2.admissible_one_eq

PrimeNumberTheoremAnd.IEANTN.FKS2Cor23Row4 · PrimeNumberTheoremAnd/IEANTN/FKS2Cor23Row4.lean:42 to 55

Source documentation

admissible_bound A 1 C R x in terms of s = √(log x): = (A / R) · s² · exp(−(C/√R)·s). The B = 1 analogue of admissible_three_halves_eq, used for the row-4 tail domination.

Exact Lean statement

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

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma admissible_one_eq (A C R x : ℝ) (hL : 0 ≤ Real.log x) (hR : 0 < R) :    admissible_bound A 1 C R x      = (A / R) * Real.sqrt (Real.log x) ^ 2        * 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 hssq : s ^ 2 = Real.log x := Real.sq_sqrt hL  have e1 : (Real.log x / R) ^ (1:ℝ) = s ^ 2 / R := by    rw [Real.rpow_one, ← hssq]  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