OAI/NumberTheory/TotientAsymptotic/FirstFailedRow.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The first failed row strictly separates the retained primes from the tail.

  1. def OAI.TotientAsymptotic.fordRowSum line 13
  2. lemma OAI.TotientAsymptotic.fordRowSum_le_previous line 16
  3. lemma OAI.TotientAsymptotic.xi_monotone line 35
  4. lemma OAI.TotientAsymptotic.first_failed_row_separates line 44
  5. lemma OAI.TotientAsymptotic.clamped_doubleLog_mono line 54
  6. lemma OAI.TotientAsymptotic.fordPrime_lt_of_coordinate_lt line 64
  7. theorem OAI.TotientAsymptotic.first_failed_row_prime_separation line 71
  8. lemma OAI.TotientAsymptotic.failed_row_coordinate_pos line 79
  9. lemma OAI.TotientAsymptotic.failed_row_index line 94
  10. lemma OAI.TotientAsymptotic.positive_ford_coordinate_lower line 102