ActualSurvivingGeometry.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Height geometry derived from the chosen actual good witnesses.

def OAI.TotientAsymptotic.leftFactorHeight line 14
def OAI.TotientAsymptotic.rightFactorHeight line 17
structure OAI.TotientAsymptotic.ComparisonHeightBounds line 20

theorem OAI.TotientAsymptotic.actual_surviving_geometry line 31

Source documentation

Both the zero and positive first-difference cases have the same concrete height geometry at their counting endpoint.

theorem actual_surviving_geometry : ∀ᶠ 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 → (87/100 : ℝ)*fordBandScale x i ≤ 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) →
    0<(collisionSurvivors p q η ξ i (collisionLastIndex x i)).card ∧
      ComparisonHeightBounds (survivingPair p q η ξ i (collisionLastIndex x i))
…

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.ComparisonHeightBounds