CollisionChoiceAbsorption.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Absorbing the complete class-choice costs in the strict exponent saving.

lemma OAI.TotientAsymptotic.smooth_choice_cost_scaled line 14
lemma OAI.TotientAsymptotic.collision_all_choice_cost line 25
theorem OAI.TotientAsymptotic.ford_band_absorbs_square line 55
Source documentation
Any fixed quadratic logarithmic cost is eventually smaller than the remaining fraction of the strict slack, uniformly for all retained bands.
```
theorem ford_band_absorbs_square (K : ℝ) : ∀ᶠ H : ℕ in atTop,
    ∀ᶠ x : ℝ in atTop, ∀ i : ℕ, i ≤ R x H → ∀ Y : ℝ,
    (87/100 : ℝ)*fordBandScale x i ≤ Y →
    K*((m x-i : ℕ) : ℝ)^2 ≤ Y/(16*((m x-i : ℕ) : ℝ)^4) := by
…
```
Mentions: OAI.TotientAsymptotic.R, OAI.TotientAsymptotic.fordBandScale, OAI.TotientAsymptotic.m