NonNormalExtensionCount.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Residual-value grouping for the large-prime half of Ford Lemma 2.8.

theorem OAI.TotientAsymptotic.non_normal_quarter_prime_count line 13

Source documentation

On a nonempty prime interval, its lower cutoff supplies the logarithm in Ford's exceptional-prime estimate.

theorem non_normal_quarter_prime_count : ∃ C : ℝ,0 < C ∧
    ∀ S x : ℝ,2 < S → 4 ≤ x → ∀ d : ℕ,0 < d → ∀ Q : Finset ℕ,
    (∀ p ∈ Q,p.Prime ∧ 4 ≤ p ∧ x^(1/4:ℝ) ≤ p ∧
      ((p-1)*d:ℕ) ≤ x ∧ ¬IsNormalPrime S p) →
    (Q.card:ℝ) ≤ C*x/(d*Real.log x)*(B (2*x))^5*(Real.log S)^(-1/6:ℝ) := by
…

Mentions: OAI.TotientAsymptotic.IsNormalPrime, OAI.TotientAsymptotic.B