CollisionPrefixFibers.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Restoring the common prefix does not multiply suffixes by witness choices.

lemma OAI.TotientAsymptotic.firstCollision_common_parts line 15
lemma OAI.TotientAsymptotic.collision_prefix_head_injective line 30
theorem OAI.TotientAsymptotic.collision_prefix_fiber_bound line 51
Source documentation
For each fixed suffix and common inner prefix, Chebyshev bounds the number of admissible heads by the reciprocal of their exact denominator.
```
theorem collision_prefix_fiber_bound : ∀ᶠ x : ℝ in atTop,
    ∀ H i : ℕ, P H ≤ H → 1 ≤ i → i ≤ R x H → ∀ t ≤ x,
    ∀ (s : PrefixDatum (R x H+1-i) × PrefixDatum (R x H+1-i)) (p : Fin (i-1) → ℕ),
    (((firstCollisionPairs x H t i).filter
        (fun q => pairSuffix q i=s ∧ tupleInnerPrefix q.1 (i-1)=p)).card : ℝ) ≤
      (10*x/Real.log x)*(prefixDenominator s.1 : ℝ)⁻¹*reciprocalShiftWeight p := by
…
```
Mentions: OAI.TotientAsymptotic.P, OAI.TotientAsymptotic.R, OAI.TotientAsymptotic.PrefixDatum, OAI.TotientAsymptotic.firstCollisionPairs, OAI.TotientAsymptotic.pairSuffix, OAI.TotientAsymptotic.tupleInnerPrefix, OAI.TotientAsymptotic.prefixDenominator, OAI.TotientAsymptotic.reciprocalShiftWeight