PrimeWindow.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Uniform largest-prime windows for the actual subpower prefix denominators.

lemma OAI.TotientAsymptotic.subpower_log_ratio line 14
lemma OAI.TotientAsymptotic.small_denominator_window line 22

theorem OAI.TotientAsymptotic.largest_prime_uniform_asymptotic line 74

Source documentation

The classical PNT is uniform over all denominators allowed by the proved basic-witness size bound, at every fixed comparable endpoint.

theorem largest_prime_uniform_asymptotic (hpnt : PrimeNumberTheoremInput)
    {a : ℝ} (ha : 0 < a) {ε : ℝ} (hε : 0 < ε) :
    ∀ᶠ x : ℝ in atTop, ∀ D t : ℝ, 1 ≤ D →
      Real.log D ≤ (Real.log x)^(4/5 : ℝ) → a*x ≤ t → t ≤ x →
      |(Nat.primeCounting ⌊1+t/D⌋₊ : ℝ)-t/(D*Real.log x)| ≤
        ε*(t/(D*Real.log x)) := by
…

Mentions: OAI.TotientAsymptotic.PrimeNumberTheoremInput, OAI.TotientAsymptotic.a, OAI.TotientAsymptotic.D