OAI/Combinatorics/Progressions/Lattices/IntegerBoxCutoffLogBounds.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.integerBoxGcdCutoff line 9
  2. def OAI.Erdos3.integerBoxNearRatio line 12
  3. def OAI.Erdos3.integerBoxPairScale line 15
  4. def OAI.Erdos3.integerBoxRetainedGap line 18
  5. theorem OAI.Erdos3.integerBoxGcdCutoff_spec line 21
  6. theorem OAI.Erdos3.integerBoxNearRatio_spec line 39
  7. theorem OAI.Erdos3.integerBoxBadPairBudget_of_cutoffs line 47
  8. theorem OAI.Erdos3.integerBoxRetainedGap_spec line 67
  9. theorem OAI.Erdos3.integerBoxGcdCutoff_le_exp line 93
  10. theorem OAI.Erdos3.integerBoxNearRatio_inverse_le_exp line 119
  11. theorem OAI.Erdos3.integerBoxPairScale_le_exp line 125
  12. theorem OAI.Erdos3.integerBoxRetainedGap_inverse_le_exp line 136
  13. theorem OAI.Erdos3.integerBoxGcdModulus_le_exp line 153