CollisionLogBudget.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Logarithmic normality losses are smaller than the final collision band.

lemma OAI.TotientAsymptotic.ford_band_log_upper line 13
theorem OAI.TotientAsymptotic.collision_log_loss_small line 52
Source documentation
The loss of one plus the logarithm of the normality factor is uniformly absorbed by one percent of the smallest retained collision band.
```
theorem collision_log_loss_small : ∀ᶠ H : ℕ in atTop, ∀ᶠ x : ℝ in atTop,
    ∀ i ≤ R x H, ∀ y : ℝ, 0 < B y → B y ≤ 2*fordBandScale x i →
    1+Real.log (3*B y) ≤ (1/100 : ℝ)*bandScale x (collisionLastIndex x i) := by
…
```
Mentions: OAI.TotientAsymptotic.R, OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.fordBandScale, OAI.TotientAsymptotic.bandScale, OAI.TotientAsymptotic.collisionLastIndex