SurvivingSlack.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Renumbering the actual surviving indices preserves the good-witness slack.

lemma OAI.TotientAsymptotic.orderEmbedding_offset_le line 12
lemma OAI.TotientAsymptotic.shifted_slack_sum line 26

theorem OAI.TotientAsymptotic.surviving_weighted_slack line 48

Source documentation

The discarded matching coordinates cannot consume slack. This is stated for the actual order embedding of survivors, with the original index offset.

theorem surviving_weighted_slack {x : ℝ} {H i p q : ℕ}
    {η ξ : RemainderDatum (L x H)}
    (hη : IsBasicRemainder x H η) (hk : collisionLastIndex x i< L x H)
    (hfirst : wholeWitnessPrime p η i≠wholeWitnessPrime q ξ i)
    (ν : ℕ → ℝ) {Y σ e : ℝ} (hY : 0< Y)
    (hbudget : (∑ r ∈ Finset.Icc (i+1) (L x H), a (r-i)*remainderCoord x η r)≤(1-σ)*Y)
    (hgrid : ∀ r (hr : r ∈ Finset.Icc 1 ((collisionSurvivors p q η ξ i (collisionLastIndex x i)).card-1)),
      ν r≤ remainderCoord x η (survivingIndex p q η ξ i (collisionLastIndex x i)
        ⟨r,by have := Finset.mem_Icc.mp hr; omega⟩)/Y+e) :
…

Mentions: OAI.TotientAsymptotic.RemainderDatum, OAI.TotientAsymptotic.L, OAI.TotientAsymptotic.IsBasicRemainder, OAI.TotientAsymptotic.collisionLastIndex, OAI.TotientAsymptotic.wholeWitnessPrime, OAI.TotientAsymptotic.a, OAI.TotientAsymptotic.remainderCoord, OAI.TotientAsymptotic.collisionSurvivors, OAI.TotientAsymptotic.survivingIndex