NormalitySmallParameter.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The elementary parameter range in Ford's exceptional-prime estimate.

lemma OAI.TotientAsymptotic.prime_count_global_upper line 12
lemma OAI.TotientAsymptotic.doubleLog_nat_pos line 41
lemma OAI.TotientAsymptotic.normality_small_parameter_factor line 48
theorem OAI.TotientAsymptotic.normality_small_parameter line 64
Source documentation
The desired exceptional-prime estimate holds throughout the small-S range using only Chebyshev's bound. The hard range is isolated rather than assumed.
```
theorem normality_small_parameter : ∃ C : ℝ, 0 < C ∧
    ∀ S : ℝ, 2 < S → ∀ n : ℕ, 3 < n → Real.log S ≤ (B n)^30 →
      ((nonNormalPrimes S n).card : ℝ) ≤
        C*n/Real.log n*(B n)^5*(Real.log S)^(-1/6:ℝ) := by
…
```
Mentions: OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.nonNormalPrimes