CollisionNormalityDomain.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The normality cutoff lies in the actual dyadic counting domain.

lemma OAI.TotientAsymptotic.cube_root_le_half line 13
theorem OAI.TotientAsymptotic.collision_normality_domain line 25
Source documentation
In particular this discharges S ≥ exp(exp 1) and S ≤ y in the published comparison lemma at every sufficiently late retained band.
```
theorem collision_normality_domain : ∀ᶠ H : ℕ in atTop, ∀ᶠ x : ℝ in atTop,
    ∀ i ≤ R x H, ∀ y : ℝ, 1 < y → fordBandScale x i/2 ≤ B y →
    Real.exp (Real.exp 1) ≤ normalityScale x i ∧
    1 ≤ B (normalityScale x i) ∧ normalityScale x i ≤ y := by
…
```
Mentions: OAI.TotientAsymptotic.R, OAI.TotientAsymptotic.fordBandScale, OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.normalityScale