ActualGridSlack.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The actual good-witness slack controls the constructed grid exponent.

lemma OAI.TotientAsymptotic.remainder_largest_factor_height_le line 14

theorem OAI.TotientAsymptotic.actual_grid_weighted_slack line 30

Source documentation

The sum uses the actual surviving indices, and retains the normalization error between the original witness coordinate and the dyadic endpoint.

theorem actual_grid_weighted_slack {x y Z δ : ℝ} {H i p q : ℕ}
    {η ξ : RemainderDatum (L x H)}
    (hη : IsBasicRemainder x H η) (hL : L x H < m x)
    (hg : GoodWitnessConditions p η) (hi : i ≤ R x H)
    (hk : collisionLastIndex x i < L x H)
    (hfirst : wholeWitnessPrime p η i ≠ wholeWitnessPrime q ξ i)
    (hh : 1 ≤ m x-i) (hBy : 0 < B y) (hδ : 0 < δ)
    (hcoord : remainderCoord x η i ≤ B y+1) (hinv : 1/B y ≤ δ)
    (ht : ComparisonHeightBounds (survivingPair p q η ξ i (collisionLastIndex x i)) (B y) Z)
    (halign : ∀ r, |leftFactorHeight (survivingPair p q η ξ i (collisionLastIndex x i)) r/B y-
      rightFactorHeight (survivingPair p q η ξ i (collisionLastIndex x i)) r/B y| ≤ (2*(r.val : ℝ)+1)*δ) :
    let t := survivingPair p q η ξ i (collisionLastIndex x i)
…

theorem OAI.TotientAsymptotic.actual_grid_exponent_saving line 89

Source documentation

The constructed cutoffs have the strict exponent saving on the actual collision witness, before the remaining polynomial factors are summed.

theorem actual_grid_exponent_saving {x y Z δ : ℝ} {H i p q : ℕ}
    {η ξ : RemainderDatum (L x H)}
    (hη : IsBasicRemainder x H η) (hL : L x H < m x)
    (hg : GoodWitnessConditions p η) (hi : i ≤ R x H)
    (hk : collisionLastIndex x i < L x H)
    (hfirst : wholeWitnessPrime p η i ≠ wholeWitnessPrime q ξ i)
    (hh : 2 ≤ m x-i) (hBy : 0 < B y) (hδ : 0 < δ)
    (hδu : δ ≤ 2/((m x-i : ℕ) : ℝ)^32)
    (hcoord : remainderCoord x η i ≤ B y+1) (hinv : 1/B y ≤ δ)
    (ht : ComparisonHeightBounds (survivingPair p q η ξ i (collisionLastIndex x i)) (B y) Z)
    (halign : ∀ r, |leftFactorHeight (survivingPair p q η ξ i (collisionLastIndex x i)) r/B y-
      rightFactorHeight (survivingPair p q η ξ i (collisionLastIndex x i)) r/B y| ≤ (2*(r.val : ℝ)+1)*δ)
…