OAI/NumberTheory/TotientAsymptotic/FordTerminalMass.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The terminal mass bounds for the actual Ford state families.

  1. lemma OAI.TotientAsymptotic.ford_cutoff_two_le line 12
  2. lemma OAI.TotientAsymptotic.ford_cutoff_B_one_le line 19
  3. theorem OAI.TotientAsymptotic.ford_terminal_mass line 25
  4. def OAI.TotientAsymptotic.oneStateTriple line 66
  5. lemma OAI.TotientAsymptotic.oneStateTriple_injective line 68
  6. theorem OAI.TotientAsymptotic.ford_terminal_mass_one line 81