OAI/NumberTheory/TotientAsymptotic/CollisionCanceled.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The canceled product and the residual integer satisfy Ford's size bounds.

  1. def OAI.TotientAsymptotic.collisionCanceledProduct line 15
  2. lemma OAI.TotientAsymptotic.canceled_surviving_product line 20
  3. lemma OAI.TotientAsymptotic.collisionCanceledProduct_pos line 33
  4. lemma OAI.TotientAsymptotic.collisionCanceledProduct_le_suffix line 46
  5. lemma OAI.TotientAsymptotic.small_suffix_factor_size line 70
  6. theorem OAI.TotientAsymptotic.collision_small_factors line 95

    Source documentation

    Both the fixed residual totient and the product of canceled shifts are small enough for the original published Ford lemma. No new counting input is used for these hypotheses.

    theorem collision_small_factors : ∀ᶠ H : ℕ in atTop, ∀ᶠ x : ℝ in atTop,
    ∀ i k p q : ℕ, 1 ≤ i → i ≤ R x H → i+2 ≤ L x H → L x H < m x →
    i ≤ k → k < L x H → ∀ η ξ : RemainderDatum (L x H),
    IsBasicRemainder x H η → 3 ≤ remainderPrime η i →
    wholeWitnessPrime p η i ≠ wholeWitnessPrime q ξ i → ∀ y : ℝ,
    ((remainderPrime η i-1 : ℕ) : ℝ) ≤ y →
    ((suffixPreimage η k).totient : ℝ) ≤ y^(1/100 : ℝ) ∧
    (collisionCanceledProduct p q η ξ i k : ℝ) ≤ y^(1/100 : ℝ) := by
…

    Mentions: OAI.TotientAsymptotic.R, OAI.TotientAsymptotic.L, OAI.TotientAsymptotic.m, OAI.TotientAsymptotic.RemainderDatum, OAI.TotientAsymptotic.IsBasicRemainder, OAI.TotientAsymptotic.remainderPrime, OAI.TotientAsymptotic.wholeWitnessPrime, OAI.TotientAsymptotic.suffixPreimage, OAI.TotientAsymptotic.collisionCanceledProduct