OAI/NumberTheory/TotientAsymptotic/FordStructureCount.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The complete unnormalized exceptional-value bound in Ford Theorem 16.

  1. lemma OAI.TotientAsymptotic.large_head_coordinate_gt_two line 17
  2. theorem OAI.TotientAsymptotic.ford_structure_value_count line 26
  3. theorem OAI.TotientAsymptotic.ford_structure_exception_count line 105
  4. theorem OAI.TotientAsymptotic.fordTheorem16_of_scale line 129

    Source documentation

    The structural published input now needs only the separately named counting-scale lower bound; its exceptional-set argument is internal.

    theorem fordTheorem16_of_scale (hscale : FordScaleBounds) : FordTheorem16Input := by
…

    Mentions: OAI.TotientAsymptotic.FordScaleBounds, OAI.TotientAsymptotic.FordTheorem16Input