SurvivingHeights.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Actual surviving factors, with uniform top and positive-coordinate bounds.

lemma OAI.TotientAsymptotic.one_lt_nat_of_doubleLog_pos line 15

theorem OAI.TotientAsymptotic.surviving_factor_heights line 21

Source documentation

Unlike the positive-coordinate band lemma, this also covers collisions whose first different prime is the largest prime of the tuple.

theorem surviving_factor_heights : ∀ᶠ H : ℕ in atTop, ∀ᶠ x : ℝ in atTop,
    ∀ i p q : ℕ, i ≤ R x H →
    ∀ η ξ : RemainderDatum (L x H), IsBasicRemainder x H η → IsBasicRemainder x H ξ →
    GoodWitnessConditions p η → GoodWitnessConditions q ξ →
    wholeWitnessPrime p η i ≠ wholeWitnessPrime q ξ i → ∀ y : ℝ,
    1<y → 0<B y → fordBandScale x i/2 ≤ B y → B y ≤ 2*fordBandScale x i →
    y^(9/10 : ℝ) ≤ wholeWitnessPrime p η i → y^(9/10 : ℝ) ≤ wholeWitnessPrime q ξ 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) →
    ∃ hb : 0<(collisionSurvivors p q η ξ i (collisionLastIndex x i)).card,
      ((9/10 : ℝ)*B y ≤ B (largestPrimeFactor
…

Mentions: OAI.TotientAsymptotic.R, OAI.TotientAsymptotic.RemainderDatum, OAI.TotientAsymptotic.L, OAI.TotientAsymptotic.IsBasicRemainder, OAI.TotientAsymptotic.GoodWitnessConditions, OAI.TotientAsymptotic.wholeWitnessPrime, OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.fordBandScale, OAI.TotientAsymptotic.collisionSurvivors, OAI.TotientAsymptotic.collisionLastIndex, OAI.TotientAsymptotic.survivingPair, OAI.TotientAsymptotic.largestPrimeFactor