ActualComparisonCutoffs.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Explicit finite cutoffs for the actual collision comparison.

def OAI.TotientAsymptotic.pairGridLabel line 16
def OAI.TotientAsymptotic.pairUpperCoordinates line 19
def OAI.TotientAsymptotic.pairLowerCoordinates line 22
lemma OAI.TotientAsymptotic.exp_exp_doubleLog line 25
lemma OAI.TotientAsymptotic.comparisonCutoffs_interval line 28

theorem OAI.TotientAsymptotic.actual_comparison_parameters line 42

Source documentation

The normalized grid constructed from a collision has all of Ford's parameter restrictions. The small integer bounds are precisely the previously proved residual and canceled-product size conclusions.

theorem actual_comparison_parameters : ∀ᶠ H : ℕ in atTop, ∀ᶠ x : ℝ in atTop,
    ∀ i p q : ℕ, i≤ R x H → L x H< m x → R x H< L x H → p.Prime →
    ∀ η ξ : RemainderDatum (L x H), IsBasicRemainder x H η → IsBasicRemainder x H ξ →
    GoodWitnessConditions p η → GoodWitnessConditions q ξ →
    tupleValue (witnessTuple p η)=tupleValue (witnessTuple q ξ) →
    wholeWitnessPrime p η i≠wholeWitnessPrime q ξ i →
    (∀ j < i, wholeWitnessPrime p η j=wholeWitnessPrime q ξ j) → ∀ 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 →
    (witnessBlockValue p η i (collisionLastIndex x i) : ℝ)≤ y →
    (collisionResidual η i : ℝ)≤ y^(1/100 : ℝ) →
    (collisionCanceledProduct p q η ξ i (collisionLastIndex x i) : ℝ)≤ y^(1/10 : ℝ) →
…