ValueCoverage.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

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