OAI/NumberTheory/TotientAsymptotic/DistinctLargestEncoding.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

Exact reconstruction and residual bounds for unequal largest primes.

  1. structure OAI.TotientAsymptotic.DistinctLargestConditions line 11
  2. def OAI.TotientAsymptotic.CrossRemoval line 27
  3. def OAI.TotientAsymptotic.distinctLargestEncoding line 32
  4. def OAI.TotientAsymptotic.distinctPrimeDecode line 37
  5. lemma OAI.TotientAsymptotic.distinctLargest_divisors line 40
  6. lemma OAI.TotientAsymptotic.distinctLargest_slots line 49
  7. lemma OAI.TotientAsymptotic.distinctLargest_decode line 53
  8. lemma OAI.TotientAsymptotic.distinctLargest_product line 60
  9. lemma OAI.TotientAsymptotic.distinctLargest_residual line 67
  10. lemma OAI.TotientAsymptotic.distinctLargest_residual_squarefree line 90