AllCollisionCount.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

Summation over all first-difference indices in the actual collision set.

lemma OAI.TotientAsymptotic.G_eventually_one_le line 15
lemma OAI.TotientAsymptotic.collision_exponential_kernel line 27
lemma OAI.TotientAsymptotic.good_collision_card_le_first_sum line 52
lemma OAI.TotientAsymptotic.firstCollisionPairs_zero line 67
lemma OAI.TotientAsymptotic.first_index_kernel_sum line 73
lemma OAI.TotientAsymptotic.head_exponential_le_block line 95
theorem OAI.TotientAsymptotic.good_collision_count line 106
Source documentation
The full ordered collision count, including every common prefix and both residual tuple factorizations, has a phase-independent vanishing error.
```
theorem good_collision_count (hford : FordLemma51Input) (hmertens : MertensProductInput)
    (hbox : FordUnitPrimeBoxInput) (hren : FordRenewalInput) :
    ∃ ε : ℕ → ℝ, Tendsto ε atTop (nhds 0) ∧
      ∀ᶠ H : ℕ in atTop, ∀ᶠ x : ℝ in atTop, ∀ t ≤ x,
      ((goodCollisionPairs x H t).card : ℝ) ≤ ε H*(x/Real.log x*G x (m x)) := by
…
```
Mentions: OAI.TotientAsymptotic.FordLemma51Input, OAI.TotientAsymptotic.MertensProductInput, OAI.TotientAsymptotic.FordUnitPrimeBoxInput, OAI.TotientAsymptotic.FordRenewalInput, OAI.TotientAsymptotic.goodCollisionPairs, OAI.TotientAsymptotic.G, OAI.TotientAsymptotic.m