ValueComparison.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.TotientAsymptotic.value_tuple_comparison line 12
theorem OAI.TotientAsymptotic.value_finite_coefficient_approximation line 36
Source documentation
The complete downstream comparison between actual distinct values and finite arithmetic coefficients, uniformly over comparable endpoints.
```
theorem value_finite_coefficient_approximation (hscale : FordScaleBounds)
    (hstruct : ExtractedStructureInput) (hpnt : PrimeNumberTheoremInput)
    (hbox : FordUnitPrimeBoxInput) (hren : FordRenewalInput) (hmertens : MertensProductInput)
    (h26 : FordLemma26Input) (h51 : FordLemma51Input) (hconc : FordCoordinateConcentrationInput)
    {a : ℝ} (ha : 0<a) :
    ∃ δ : ℕ → ℝ, Tendsto δ atTop (nhds 0) ∧
      ∀ᶠ H : ℕ in atTop, ∀ ε : ℝ, 0<ε → ∀ᶠ x : ℝ in atTop,
      ∀ t : ℝ, a*x ≤ t → t ≤ x →
        |V t/tupleNormalization x-(t/x)*AH H (fun _ => 1) (theta x)| ≤ δ H+ε := by
…
```
Mentions: OAI.TotientAsymptotic.FordScaleBounds, OAI.TotientAsymptotic.ExtractedStructureInput, OAI.TotientAsymptotic.PrimeNumberTheoremInput, OAI.TotientAsymptotic.FordUnitPrimeBoxInput, OAI.TotientAsymptotic.FordRenewalInput, OAI.TotientAsymptotic.MertensProductInput, OAI.TotientAsymptotic.FordLemma26Input, OAI.TotientAsymptotic.FordLemma51Input, OAI.TotientAsymptotic.FordCoordinateConcentrationInput, OAI.TotientAsymptotic.a, OAI.TotientAsymptotic.V, OAI.TotientAsymptotic.AH, OAI.TotientAsymptotic.theta