CollisionHeadCount.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The complete comparison estimate for pairs with different head primes.

def OAI.TotientAsymptotic.headCollisionPairs line 14
lemma OAI.TotientAsymptotic.head_collision_block line 18
theorem OAI.TotientAsymptotic.head_collision_count line 38
Source documentation
All grids, canceled index sets, canceled primes, and both residual tuple factorizations are summed. There is no fixed-prefix cost at index zero.
```
theorem head_collision_count (hford : FordLemma51Input) (hmertens : MertensProductInput) :
    ∀ᶠ H : ℕ in atTop, ∀ᶠ x : ℝ in atTop, ∀ t ≤ x,
    ((headCollisionPairs x H t).card : ℝ) ≤
      x/Real.log x*Real.exp (-B x/(8*(m x : ℝ)^4)) := by
…
```
Mentions: OAI.TotientAsymptotic.FordLemma51Input, OAI.TotientAsymptotic.MertensProductInput, OAI.TotientAsymptotic.headCollisionPairs, OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.m