OAI/NumberTheory/TotientAsymptotic/ChosenCollision.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TotientAsymptotic.chosenRemainder line 13
2. lemma OAI.TotientAsymptotic.chosenRemainder_spec line 17
3. lemma OAI.TotientAsymptotic.chosenRemainder_tuple line 25
4. lemma OAI.TotientAsymptotic.chosenRemainder_good line 31
5. lemma OAI.TotientAsymptotic.wholeWitnessPrime_tuple line 35
6. lemma OAI.TotientAsymptotic.chosen_collision_first line 42
7. def OAI.TotientAsymptotic.goodCollisionPairs line 63
8. theorem OAI.TotientAsymptotic.good_collision_surviving_identity line 70

   Source documentation

   All the qualitative comparison data are extracted from the actual finite collision set, with the universal good-witness condition preserved.

   theorem good_collision_surviving_identity {x t : ℝ} {H : ℕ}
       (hPH : P H < H) (hP : 1 ≤ P H) (hHm : H ≤ m x)
       (hind : ∀ i ≤ R x H, i+collisionCutoff (m x-i) < L x H)
       {τ σ : TotientTuple (R x H)} (hq : (τ,σ) ∈ goodCollisionPairs x H t) :
       ∃ i ≤ R x H,
         0 < (collisionSurvivors τ.head σ.head (chosenRemainder x H τ.tail)
           (chosenRemainder x H σ.tail) i (collisionLastIndex x i)).card ∧
         (collisionSurvivors τ.head σ.head (chosenRemainder x H τ.tail)
           (chosenRemainder x H σ.tail) i (collisionLastIndex x i)).card ≤
           collisionCutoff (m x-i)+1 ∧
         (collisionResidual (chosenRemainder x H τ.tail) i)*
           shiftedProduct (survivingPair τ.head σ.head (chosenRemainder x H τ.tail)
   …

   Mentions: OAI.TotientAsymptotic.P, OAI.TotientAsymptotic.m, OAI.TotientAsymptotic.R, OAI.TotientAsymptotic.collisionCutoff, OAI.TotientAsymptotic.L, OAI.TotientAsymptotic.TotientTuple, OAI.TotientAsymptotic.goodCollisionPairs, OAI.TotientAsymptotic.collisionSurvivors, OAI.TotientAsymptotic.chosenRemainder, OAI.TotientAsymptotic.collisionLastIndex, OAI.TotientAsymptotic.collisionResidual, OAI.TotientAsymptotic.shiftedProduct, OAI.TotientAsymptotic.survivingPair