OAI/NumberTheory/TotientAsymptotic/FordCollisionCutoffs.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The actual Ford scales satisfy the cutoff hypotheses used for good collisions.

  1. lemma OAI.TotientAsymptotic.ford_band_lower line 13
  2. lemma OAI.TotientAsymptotic.next_band_below_ford_cutoff line 28
  3. theorem OAI.TotientAsymptotic.basic_residual_ford_smooth line 40
  4. lemma OAI.TotientAsymptotic.ford_band_polynomial_lower line 57
  5. lemma OAI.TotientAsymptotic.cube_root_le_scaled line 80
  6. lemma OAI.TotientAsymptotic.ford_collision_layer_ratio line 102
  7. lemma OAI.TotientAsymptotic.scaled_cube_root_lt line 125
  8. theorem OAI.TotientAsymptotic.collision_normality_below_cutoff line 144

    Source documentation

    The normality scale lies strictly below the smooth-residual cutoff, uniformly for all retained collision indices.

    theorem collision_normality_below_cutoff : ∀ᶠ H : ℕ in atTop,
    ∀ᶠ x : ℝ in atTop, ∀ i ≤ R x H,
      normalityScale x i < collisionSmoothCutoff x i := by
…

    Mentions: OAI.TotientAsymptotic.R, OAI.TotientAsymptotic.normalityScale, OAI.TotientAsymptotic.collisionSmoothCutoff

  9. theorem OAI.TotientAsymptotic.collision_residual_below_cutoff line 164