OAI/NumberTheory/TotientAsymptotic/FordBandGeometry.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Actual cutoff geometry for the application of Ford's interval sieve.

  1. lemma OAI.TotientAsymptotic.ford_cutoff_antitone line 12
  2. lemma OAI.TotientAsymptotic.ford_cutoff_ge_S line 21
  3. lemma OAI.TotientAsymptotic.ford_cutoff_le_y line 25
  4. lemma OAI.TotientAsymptotic.largestPrimeFactor_band line 29
  5. lemma OAI.TotientAsymptotic.band_factor_ge_two line 44
  6. def OAI.TotientAsymptotic.fordFactorState line 59
  7. lemma OAI.TotientAsymptotic.lower_fordFactorState line 64
  8. lemma OAI.TotientAsymptotic.stateBand_fordFactorState line 74