QuarterPrimeCount.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The quarter-power prime interval used in Ford’s global counting argument. Chebyshev's library theorem suffices for the upper bound; no PNT input is used here.

theorem OAI.TotientAsymptotic.quarter_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 quarter_prime_count_upper :
    ∀ᶠ x : ℝ in atTop, ∀ D : ℕ, 0 < D → ∀ Q : Finset ℕ,
      (∀ p ∈ Q, p.Prime ∧ x^(1/4 : ℝ) ≤ p ∧ ((p-1)*D : ℕ) ≤ x) →
      (Q.card : ℝ) ≤ 32*x/((D : ℝ)*Real.log x) := by
…
```
Mentions: OAI.TotientAsymptotic.D