ValueLower.lean`

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.TotientAsymptotic.tuple_excess_negligible line 14
Source documentation
The actual count can exceed the number of represented values only by the discarded tuples and the collision error, both already proved small.
```
theorem tuple_excess_negligible (hbox : FordUnitPrimeBoxInput) (hren : FordRenewalInput)
    (hmertens : MertensProductInput) (h26 : FordLemma26Input) (h51 : FordLemma51Input) :
    ∃ δ : ℕ → ℝ, Tendsto δ atTop (nhds 0) ∧
      ∀ᶠ H : ℕ in atTop, ∀ᶠ x : ℝ in atTop, ∀ t ≤ x,
        ((tupleFinset x H t).card : ℝ)-V t ≤ δ H*tupleNormalization x := by
…
```
Mentions: OAI.TotientAsymptotic.FordUnitPrimeBoxInput, OAI.TotientAsymptotic.FordRenewalInput, OAI.TotientAsymptotic.MertensProductInput, OAI.TotientAsymptotic.FordLemma26Input, OAI.TotientAsymptotic.FordLemma51Input, OAI.TotientAsymptotic.tupleFinset, OAI.TotientAsymptotic.V
theorem OAI.TotientAsymptotic.normalized_value_coefficient_lower line 30
Source documentation
The lower half of the main count comparison follows from actual collision and discard bounds, with no exceptional-value coverage premise.
```
theorem normalized_value_coefficient_lower (hpnt : PrimeNumberTheoremInput)
    (hbox : FordUnitPrimeBoxInput) (hren : FordRenewalInput) (hmertens : MertensProductInput)
    (h26 : FordLemma26Input) (h51 : FordLemma51Input) (hconc : FordCoordinateConcentrationInput) :
    ∃ δ : ℕ → ℝ, Tendsto δ atTop (nhds 0) ∧
      ∀ᶠ H : ℕ in atTop, ∀ ε : ℝ, 0 < ε → ∀ᶠ x : ℝ in atTop,
        AH H (fun _ => 1) (theta x)-δ H-ε ≤ normalizedCount V x := by
…
```
Mentions: OAI.TotientAsymptotic.PrimeNumberTheoremInput, OAI.TotientAsymptotic.FordUnitPrimeBoxInput, OAI.TotientAsymptotic.FordRenewalInput, OAI.TotientAsymptotic.MertensProductInput, OAI.TotientAsymptotic.FordLemma26Input, OAI.TotientAsymptotic.FordLemma51Input, OAI.TotientAsymptotic.FordCoordinateConcentrationInput, OAI.TotientAsymptotic.AH, OAI.TotientAsymptotic.theta, OAI.TotientAsymptotic.normalizedCount, OAI.TotientAsymptotic.V