OAI/NumberTheory/TotientAsymptotic/CollisionCutoff.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TotientAsymptotic.collisionCutoff line 14
2. lemma OAI.TotientAsymptotic.collisionCutoff_bounds line 16
3. lemma OAI.TotientAsymptotic.collisionCutoff_div_tendsto line 22
4. lemma OAI.TotientAsymptotic.collisionCutoff_eventually_small line 37
5. lemma OAI.TotientAsymptotic.rho_collisionCutoff_bounds line 46
6. lemma OAI.TotientAsymptotic.collision_layer_ratio line 75

   Source documentation

   Phase-uniform comparison of the layer at the first collision and the last layer retained by the logarithmic cutoff.

   lemma collision_layer_ratio {h : ℕ} (hh : 1 ≤ h)
       (hJ : 2*collisionCutoff h ≤ h) (s : ℝ) :
       rho/(2*(h : ℝ)^20) ≤
         (alpha s*(h-collisionCutoff h : ℕ)/(rho^(h-collisionCutoff h))) /
           (alpha s*h/rho^h) ∧
       (alpha s*(h-collisionCutoff h : ℕ)/(rho^(h-collisionCutoff h))) /
           (alpha s*h/rho^h) ≤ 1/(h : ℝ)^18 := by
   …

   Mentions: OAI.TotientAsymptotic.collisionCutoff, OAI.TotientAsymptotic.rho, OAI.TotientAsymptotic.alpha