OAI/NumberTheory/TotientAsymptotic/CollisionClassData.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.TotientAsymptotic.canceledIndices line 14
2. def OAI.TotientAsymptotic.canceledPrimesAt line 16
3. lemma OAI.TotientAsymptotic.canceledIndices_eq line 21
4. lemma OAI.TotientAsymptotic.canceledPrimesAt_product line 28
5. lemma OAI.TotientAsymptotic.comparisonPairAt_survivors line 44
6. lemma OAI.TotientAsymptotic.fixed_primes_of_canceled_data line 52

   Source documentation

   The fixed pref and the canceled-prime list provide precisely the fixed-coordinate hypothesis needed to recover an actual pair from Ford data.

   lemma fixed_primes_of_canceled_data {x : ℝ} {H i k : ℕ} (I : Finset ℕ)
       (τ σ : TotientTuple (R x H)) (pref : ℕ → ℕ)
       (v : Fin (canceledIndices i k I).card → ℕ)
       (hI : collisionSurvivors τ.head σ.head (chosenRemainder x H τ.tail)
         (chosenRemainder x H σ.tail) i k=I)
       (hpref : ∀ j < i, wholeWitnessPrime τ.head (chosenRemainder x H τ.tail) j=pref j ∧
         wholeWitnessPrime σ.head (chosenRemainder x H σ.tail) j=pref j)
       (hv : canceledPrimesAt x H i k I τ=v) :
       ∀ j ≤ k, j ∉ I →
         wholeWitnessPrime τ.head (chosenRemainder x H τ.tail) j =
           (if h : j ∈ canceledIndices i k I then
             v ((canceledIndices i k I).orderIsoOfFin rfl |>.symm ⟨j,h⟩) else pref j) ∧
   …

   Mentions: OAI.TotientAsymptotic.TotientTuple, OAI.TotientAsymptotic.R, OAI.TotientAsymptotic.canceledIndices, OAI.TotientAsymptotic.collisionSurvivors, OAI.TotientAsymptotic.chosenRemainder, OAI.TotientAsymptotic.wholeWitnessPrime, OAI.TotientAsymptotic.canceledPrimesAt