CandidateComparison.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.TotientAsymptotic.candidate_value_comparison line 14
Source documentation
The same negligible error controls every least-preimage interval; it counts all exceptional values and all tuples above them.
```
theorem candidate_value_comparison (hscale : FordScaleBounds)
    (hstruct : ExtractedStructureInput)
    (hbox : FordUnitPrimeBoxInput) (hren : FordRenewalInput) (hmertens : MertensProductInput)
    (h26 : FordLemma26Input) (h51 : FordLemma51Input) :
    ∃ δ : ℕ → ℝ, Tendsto δ atTop (nhds 0) ∧
      ∀ᶠ H : ℕ in atTop, ∀ ε : ℝ, 0 < ε → ∀ᶠ x : ℝ in atTop, ∀ k : ℕ,
        |((candidateTuples x H k).card : ℝ)-N k x| ≤ (δ H+ε)*tupleNormalization x := by
…
```
Mentions: OAI.TotientAsymptotic.FordScaleBounds, OAI.TotientAsymptotic.ExtractedStructureInput, OAI.TotientAsymptotic.FordUnitPrimeBoxInput, OAI.TotientAsymptotic.FordRenewalInput, OAI.TotientAsymptotic.MertensProductInput, OAI.TotientAsymptotic.FordLemma26Input, OAI.TotientAsymptotic.FordLemma51Input, OAI.TotientAsymptotic.candidateTuples, OAI.TotientAsymptotic.N