OAI/NumberTheory/TotientAsymptotic/ComparisonGridFromHeights.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.TotientAsymptotic.collisionMesh_le_hundredth line 11
2. theorem OAI.TotientAsymptotic.comparison_grid_from_heights line 23

   Source documentation

   The grid label is chosen from the actual paired largest factors. Every width and separation restriction is proved here, including the one-prime case.

   theorem comparison_grid_from_heights {b h : ℕ} {t : ShiftedPair b} {Y Z δ : ℝ}
       (hb : 0<b) (hbh : b≤h) (hh : 4≤h) (hY : 0<Y) (_hZ : 0<Z) (hZY : Z≤Y)
       (hδ : 0<δ) (hδu : δ≤2/(h : ℝ)^32)
       (hmargin : (2*(h : ℝ)+10)*δ < (1/10 : ℝ)*Z/Y)
       (ht : ComparisonHeightBounds t Y Z)
       (halign : ∀ r, |leftFactorHeight t r/Y-rightFactorHeight t r/Y| ≤
         (2*(r.val : ℝ)+1)*δ) :
       let u := fun r => leftFactorHeight t r/Y
   …

   Mentions: OAI.TotientAsymptotic.ShiftedPair, OAI.TotientAsymptotic.ComparisonHeightBounds, OAI.TotientAsymptotic.leftFactorHeight, OAI.TotientAsymptotic.rightFactorHeight