SurvivingComparison.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Assemble Ford's pointwise comparison hypotheses for actual surviving lists.

lemma OAI.TotientAsymptotic.normal_prime_omega_below line 14

theorem OAI.TotientAsymptotic.surviving_comparison_conditions line 32

Source documentation

All pointwise hypotheses, including the large-prime-part condition, follow for the actual canceled lists once their ordered factor intervals are chosen. The remaining interval construction and summation are separate obligations.

theorem surviving_comparison_conditions : ∀ᶠ y : ℝ in atTop,
    ∀ {x : ℝ} {H i p q : ℕ} {η ξ : RemainderDatum (L x H)},
    IsBasicRemainder x H η → IsBasicRemainder x H ξ → p.Prime →
    L x H < m x → R x H < L x H → i ≤ R x H → collisionLastIndex x i < L x H →
    tupleValue (witnessTuple p η)=tupleValue (witnessTuple q ξ) →
    wholeWitnessPrime p η i ≠ wholeWitnessPrime q ξ i →
    (∀ j < i, wholeWitnessPrime p η j=wholeWitnessPrime q ξ j) →
    GoodWitnessConditions p η → GoodWitnessConditions q ξ →
    ∀ Y U : ℕ → ℝ,
    1 < normalityScale x i → 0 ≤ B (normalityScale x i) → normalityScale x i ≤ y →
    Y (collisionSurvivors p q η ξ i (collisionLastIndex x i)).card=collisionSmoothCutoff x i →
    (∀ j : Fin (collisionSurvivors p q η ξ i (collisionLastIndex x i)).card,
…