SurvivingBands.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Strict ordering of the actual surviving largest factors and their cutoff.

lemma OAI.TotientAsymptotic.lt_of_doubleLog_lt line 14

theorem OAI.TotientAsymptotic.surviving_largest_factor_bands line 21

Source documentation

The bands used to align the collision primes are disjoint even after the normality losses, and all lie above the smooth-residual cutoff.

theorem surviving_largest_factor_bands : ∀ᶠ H : ℕ in atTop, ∀ᶠ x : ℝ in atTop,
    ∀ i p q : ℕ, 1 ≤ i → i ≤ R x H → L x H < m x →
    ∀ η ξ : RemainderDatum (L x H), IsBasicRemainder x H η → IsBasicRemainder x H ξ →
    GoodWitnessConditions p η → GoodWitnessConditions q ξ → ∀ y : ℝ,
    1 < normalityScale x i → 0 ≤ B (normalityScale x i) → normalityScale x i ≤ y →
    0 < B y → B y ≤ 2*fordBandScale x i →
    (∀ r : Fin (collisionSurvivors p q η ξ i (collisionLastIndex x i)).card,
      ((survivingPair p q η ξ i (collisionLastIndex x i)).left r-1 : ℕ) ≤ y ∧
      ((survivingPair p q η ξ i (collisionLastIndex x i)).right r-1 : ℕ) ≤ y) →
    (∀ r, collisionSmoothCutoff x i <
      min (largestPrimeFactor ((survivingPair p q η ξ i (collisionLastIndex x i)).left r-1) : ℝ)
        (largestPrimeFactor ((survivingPair p q η ξ i (collisionLastIndex x i)).right r-1) : ℝ)) ∧
…