OAI/NumberTheory/TotientAsymptotic/CollisionTuples.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Actual tuples, their basic witnesses, and the first differing prime.

  1. structure OAI.TotientAsymptotic.TotientTuple line 13
  2. def OAI.TotientAsymptotic.tuplePrimes line 17
  3. def OAI.TotientAsymptotic.tupleValue line 20
  4. def OAI.TotientAsymptotic.IsBasicTuple line 23
  5. lemma OAI.TotientAsymptotic.basic_prefix_data_positive line 26
  6. lemma OAI.TotientAsymptotic.basic_tuple_primes line 41
  7. lemma OAI.TotientAsymptotic.basic_tuple_value_pos line 48
  8. lemma OAI.TotientAsymptotic.tuple_eq_of_value_and_primes line 53
  9. lemma OAI.TotientAsymptotic.basic_collision_first_difference line 75
  10. lemma OAI.TotientAsymptotic.tuple_collision_suffix_identity line 98

    Source documentation

    The common displayed prefix cancels before the comparison estimate is applied. The remaining product still contains the true tail totient.

    lemma tuple_collision_suffix_identity {R : ℕ} {τ σ : TotientTuple R}
    (hp : ∀ i, 2 ≤ tuplePrimes τ i) (hv : tupleValue τ = tupleValue σ)
    (i : Fin (R+1)) (hcommon : ∀ j, j < i → tuplePrimes τ j = tuplePrimes σ j) :
    τ.tail.d*(∏ j ∈ Finset.Ici i, (tuplePrimes τ j-1)) =
      σ.tail.d*(∏ j ∈ Finset.Ici i, (tuplePrimes σ j-1)) := by
…

    Mentions: OAI.TotientAsymptotic.R, OAI.TotientAsymptotic.TotientTuple, OAI.TotientAsymptotic.tuplePrimes, OAI.TotientAsymptotic.tupleValue