LargestPrimeCount.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Uniform upper counting of the largest prime after a remainder is fixed. Chebyshev's library theorem suffices for the upper bound; no PNT input is used here.

theorem OAI.TotientAsymptotic.largest_prime_count_upper line 16
Source documentation
The largest-prime restriction makes the logarithm of every nonempty counting interval comparable to log x, uniformly in its integer denominator.
```
theorem largest_prime_count_upper :
    ∀ᶠ x : ℝ in atTop, ∀ D : ℕ, 0 < D → ∀ Q : Finset ℕ,
      (∀ p ∈ Q, p.Prime ∧ x^(9/10 : ℝ) ≤ p ∧ ((p-1)*D : ℕ) ≤ x) →
      (Q.card : ℝ) ≤ 10*x/((D : ℝ)*Real.log x) := by
…
```
Mentions: OAI.TotientAsymptotic.D