CollisionSuffixSize.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Uniform size of the actual suffix following a first differing prime.

lemma OAI.TotientAsymptotic.collision_coarse_sizes line 14
lemma OAI.TotientAsymptotic.collision_tail_ratio_decay line 58
theorem OAI.TotientAsymptotic.collision_tail_log_small line 79
Source documentation
After any retained positive index, the whole residual preimage, including its possibly repeated final prime, has logarithm at most one per mille of the logarithm of the first prime.
```
theorem collision_tail_log_small : ∀ᶠ H : ℕ in atTop, ∀ᶠ x : ℝ in atTop,
    ∀ i : ℕ, 1 ≤ i → i ≤ R x H → i+2 ≤ L x H → L x H < m x →
    ∀ η : RemainderDatum (L x H), IsBasicRemainder x H η →
    Real.log (suffixPreimage η i : ℝ) ≤ (1/1000 : ℝ)*Real.log (remainderPrime η i : ℝ) := by
…
```
Mentions: OAI.TotientAsymptotic.R, OAI.TotientAsymptotic.L, OAI.TotientAsymptotic.m, OAI.TotientAsymptotic.RemainderDatum, OAI.TotientAsymptotic.IsBasicRemainder, OAI.TotientAsymptotic.suffixPreimage, OAI.TotientAsymptotic.remainderPrime