SurvivingBlockSize.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Exact block values and bounds for both surviving shifted-prime lists.

def OAI.TotientAsymptotic.witnessBlockValue line 12
lemma OAI.TotientAsymptotic.witnessBlockValue_zero line 15
lemma OAI.TotientAsymptotic.witnessBlockValue_positive line 20

theorem OAI.TotientAsymptotic.surviving_shift_le_block line 39

Source documentation

A dyadic bound on the full block bounds every surviving shift on either side, after cancellation and with both residual factors retained.

theorem surviving_shift_le_block {x y : ℝ} {H i k p q : ℕ}
    {η ξ : RemainderDatum (L x H)}
    (hη : IsBasicRemainder x H η) (hξ : IsBasicRemainder x H ξ) (hp : p.Prime)
    (hL : L x H < m x) (hR : R x H < L x H) (hk : k < L x H) (hik : i ≤ k)
    (hv : tupleValue (witnessTuple p η)=tupleValue (witnessTuple q ξ))
    (hfirst : wholeWitnessPrime p η i ≠ wholeWitnessPrime q ξ i)
    (hcommon : ∀ j < i, wholeWitnessPrime p η j=wholeWitnessPrime q ξ j)
    (hsize : (witnessBlockValue p η i k : ℝ) ≤ y) :
    ∀ r : Fin (collisionSurvivors p q η ξ i k).card,
      ((survivingPair p q η ξ i k).left r-1 : ℕ) ≤ y ∧
      ((survivingPair p q η ξ i k).right r-1 : ℕ) ≤ y := by
…

Mentions: OAI.TotientAsymptotic.RemainderDatum, OAI.TotientAsymptotic.L, OAI.TotientAsymptotic.IsBasicRemainder, OAI.TotientAsymptotic.m, OAI.TotientAsymptotic.R, OAI.TotientAsymptotic.tupleValue, OAI.TotientAsymptotic.witnessTuple, OAI.TotientAsymptotic.wholeWitnessPrime, OAI.TotientAsymptotic.witnessBlockValue, OAI.TotientAsymptotic.collisionSurvivors, OAI.TotientAsymptotic.survivingPair