OAI/NumberTheory/TotientAsymptotic/CollisionGrid.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TotientAsymptotic.collisionGridIndex line 13
2. def OAI.TotientAsymptotic.collisionGridLower line 15
3. def OAI.TotientAsymptotic.collisionGridUpper line 17
4. lemma OAI.TotientAsymptotic.collision_grid_lower_bounds line 19
5. theorem OAI.TotientAsymptotic.collision_grid_enclosure line 33

   Source documentation

   The paired largest factors fit in one of finitely many grid intervals. The width retains the full alignment error and one rounding cell.

   theorem collision_grid_enclosure {δ u v : ℝ} {J : ℕ}
       (hδ : 0 < δ) (hu : 0 ≤ u) (hv : 0 ≤ v)
       (hclose : |u-v| ≤ (2*(J : ℝ)+1)*δ) :
       let n := collisionGridIndex δ u v
   …

   Mentions: OAI.TotientAsymptotic.collisionGridIndex

6. lemma OAI.TotientAsymptotic.collisionGridIndex_le line 57
7. lemma OAI.TotientAsymptotic.collision_grid_separated line 63

   Source documentation

   Disjoint largest-factor bands remain strictly ordered after gridding, provided their gap exceeds the explicit alignment and rounding costs.

   lemma collision_grid_separated {δ u v u' v' : ℝ} {J : ℕ}
       (hδ : 0 < δ) (hu : 0 ≤ u) (hv : 0 ≤ v) (hu' : 0 ≤ u') (hv' : 0 ≤ v')
       (hclose' : |u'-v'| ≤ (2*(J : ℝ)+1)*δ)
       (hgap : max u' v'+(2*(J : ℝ)+4)*δ < min u v) :
       collisionGridUpper δ J (collisionGridIndex δ u' v') <
         collisionGridLower δ (collisionGridIndex δ u v) := by
   …

   Mentions: OAI.TotientAsymptotic.collisionGridUpper, OAI.TotientAsymptotic.collisionGridIndex, OAI.TotientAsymptotic.collisionGridLower

8. def OAI.TotientAsymptotic.collisionGridFamilies line 73
9. lemma OAI.TotientAsymptotic.collisionGridFamilies_card line 76
10. lemma OAI.TotientAsymptotic.collisionGridFamilies_mem line 80