BasicExceptionCount.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.TotientAsymptotic.basic_exception_values_negligible line 13
Source documentation
All uncovered values are controlled by the published Ford extraction and the independently proved cofactor and elementary exclusions.
```
theorem basic_exception_values_negligible (_hscale : FordScaleBounds)
    (hstruct : ExtractedStructureInput)
    (hbox : FordUnitPrimeBoxInput) (hren : FordRenewalInput) (hmertens : MertensProductInput) :
    ∃ δ : ℕ → ℝ, Tendsto δ atTop (nhds 0) ∧
      ∀ᶠ H : ℕ in atTop, ∀ ε : ℝ, 0<ε → ∀ᶠ x : ℝ in atTop,
        ((basicExceptionValues x H).card : ℝ) ≤ (δ H+ε)*tupleNormalization x := by
…
```
Mentions: OAI.TotientAsymptotic.FordScaleBounds, OAI.TotientAsymptotic.ExtractedStructureInput, OAI.TotientAsymptotic.FordUnitPrimeBoxInput, OAI.TotientAsymptotic.FordRenewalInput, OAI.TotientAsymptotic.MertensProductInput, OAI.TotientAsymptotic.basicExceptionValues