CollisionGridCount.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The complete family of alignment grids has only exponential-square cost.

lemma OAI.TotientAsymptotic.collisionMesh_inverse_bound line 15
lemma OAI.TotientAsymptotic.alignment_grid_card_bound line 24
theorem OAI.TotientAsymptotic.collision_grid_card_uniform line 51
Source documentation
The source's grid-choice cost is bounded uniformly in the phase by exp (26 h²) for all retained positive or zero collision indices.
```
theorem collision_grid_card_uniform : ∀ᶠ H : ℕ in atTop, ∀ᶠ x : ℝ in atTop,
    ∀ i ≤ R x H, ∀ y : ℝ, 1 ≤ B (normalityScale x i) → 1 ≤ B y →
    B y ≤ 2*fordBandScale x i → ∀ b ≤ m x-i,
    ((collisionGridFamilies (collisionMesh x y i) b).card : ℝ) ≤
      Real.exp (26*((m x-i : ℕ) : ℝ)^2) := by
…
```
Mentions: OAI.TotientAsymptotic.R, OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.normalityScale, OAI.TotientAsymptotic.fordBandScale, OAI.TotientAsymptotic.m, OAI.TotientAsymptotic.collisionGridFamilies, OAI.TotientAsymptotic.collisionMesh