PublishedPrimeCount.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The classical prime number theorem, in precisely the epsilon form used here. Hadamard and de la Vallée Poussin (1896); for a numbered, accessible statement see Terence Tao, 254A, Notes 2: Complex-analytic multiplicative number theory (9 December 2014), Exercise 40, following Corollary 39: https://terrytao.wordpress.com/2014/12/09/254a-notes-2-complex-analytic-multiplicative-number-theory/ Only pi(y) ~ y/log(y) is retained from the stronger published estimate.

def OAI.TotientAsymptotic.PrimeNumberTheoremInput line 20

lemma OAI.TotientAsymptotic.prime_count_change_scale line 26

Source documentation

A deterministic change of the logarithm and the endpoint in a prime count. Its hypotheses are later verified uniformly over all prefix data.

lemma prime_count_change_scale {x y z δ : ℝ}
    (hL : 0 < Real.log x) (hz : 0 ≤ z) (hδ : 0 ≤ δ) (hδsmall : δ ≤ 1/4)
    (hlog : (1-δ)*Real.log x ≤ Real.log y ∧ Real.log y ≤ (1+δ)*Real.log x)
    (hy : z ≤ y ∧ y ≤ (1+δ)*z)
    (hp : |(Nat.primeCounting ⌊y⌋₊ : ℝ)-y/Real.log y| ≤ δ*(y/Real.log y)) :
    |(Nat.primeCounting ⌊y⌋₊ : ℝ)-z/Real.log x| ≤ 6*δ*(z/Real.log x) := by
…