OAI/NumberTheory/TotientAsymptotic/TupleSuffix.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Actual tuple suffixes, with the common prefix removed exactly once.

  1. def OAI.TotientAsymptotic.tupleSuffix line 11
  2. def OAI.TotientAsymptotic.pairSuffix line 15
  3. lemma OAI.TotientAsymptotic.chosen_whole_prime line 18
  4. theorem OAI.TotientAsymptotic.tupleSuffix_recovered line 29

    Source documentation

    Comparison primes and residual tuples recover only the suffix being counted; the earlier common prefix is irrelevant to this reconstruction.

    theorem tupleSuffix_recovered {x t : ℝ} {H i k : ℕ}
    {τ σ : TotientTuple (R x H)} (hτ : IsBasicTuple x H t τ) (hσ : IsBasicTuple x H t σ)
    (hL : L x H < m x) (hkL : k < L x H) (hiR : i ≤ R x H)
    (hknown : ∀ r ∈ Finset.Icc i k,
      wholeWitnessPrime τ.head (chosenRemainder x H τ.tail) r =
        wholeWitnessPrime σ.head (chosenRemainder x H σ.tail) r)
    (hdata : residualTupleData (chosenRemainder x H τ.tail) k =
      residualTupleData (chosenRemainder x H σ.tail) k) :
    tupleSuffix τ i=tupleSuffix σ i := by
…

    Mentions: OAI.TotientAsymptotic.TotientTuple, OAI.TotientAsymptotic.R, OAI.TotientAsymptotic.IsBasicTuple, OAI.TotientAsymptotic.L, OAI.TotientAsymptotic.m, OAI.TotientAsymptotic.wholeWitnessPrime, OAI.TotientAsymptotic.chosenRemainder, OAI.TotientAsymptotic.residualTupleData, OAI.TotientAsymptotic.tupleSuffix