OAI/NumberTheory/TotientAsymptotic/CollisionGridScale.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Polynomially small normalized alignment mesh at each actual collision cut.

  1. lemma OAI.TotientAsymptotic.cube_root_le_div_pow line 13
  2. def OAI.TotientAsymptotic.collisionMesh line 33
  3. lemma OAI.TotientAsymptotic.collisionMesh_pos line 36
  4. theorem OAI.TotientAsymptotic.collisionMesh_bound line 46

    Source documentation

    The actual normalized alignment error is smaller than an arbitrary fixed polynomial mesh; exponent 32 suffices for the retained collision grid.

    theorem collisionMesh_bound : ∀ᶠ H : ℕ in atTop, ∀ᶠ x : ℝ in atTop,
    ∀ i ≤ R x H, ∀ y : ℝ, 0 < B y → fordBandScale x i/2 ≤ B y →
    collisionMesh x y i ≤ 2/((m x-i : ℕ) : ℝ)^32 := by
…

    Mentions: OAI.TotientAsymptotic.R, OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.fordBandScale, OAI.TotientAsymptotic.collisionMesh, OAI.TotientAsymptotic.m