NormalPrimeMass.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Derive the exceptional reciprocal-prime mass from Ford's count.

lemma OAI.TotientAsymptotic.nonNormalPrime_ge_three line 14
lemma OAI.TotientAsymptotic.dyadic_shift_lower line 23
theorem OAI.TotientAsymptotic.non_normal_prime_mass line 32
Source documentation
The only arithmetic input is the literal count in Ford Lemma 2.6. Dyadic summation supplies its needed reciprocal-weight consequence.
```
theorem non_normal_prime_mass (hford : FordLemma26Input) :
    ∃ C : ℝ, 0 < C ∧ ∀ S : ℝ, 2 < S → 0 ≤ B S → ∀ N : ℕ, 4 ≤ N →
      let L := Nat.clog 2 N
…
```
Mentions: OAI.TotientAsymptotic.FordLemma26Input, OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.N, OAI.TotientAsymptotic.L