OAI/Combinatorics/Progressions/Dynamics/DilationBudgets.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.DilationBudget.height line 12
  2. def OAI.Erdos3.DilationBudget.shift line 14
  3. def OAI.Erdos3.DilationBudget.ambient line 16
  4. def OAI.Erdos3.DilationBudget.quotient line 19
  5. def OAI.Erdos3.DilationBudget.common line 21
  6. def OAI.Erdos3.DilationBudget.reconstruction line 24
  7. def OAI.Erdos3.DilationBudget.total line 27
  8. theorem OAI.Erdos3.DilationBudget.shift_bounds line 30
  9. theorem OAI.Erdos3.DilationBudget.ambient_bounds line 36
  10. theorem OAI.Erdos3.DilationBudget.quotient_bounds line 48
  11. theorem OAI.Erdos3.DilationBudget.common_bounds line 58
  12. theorem OAI.Erdos3.DilationBudget.reconstruction_bounds line 69
  13. theorem OAI.Erdos3.DilationBudget.observable_bound line 75
  14. theorem OAI.Erdos3.DilationBudget.total_bounds line 94
  15. theorem OAI.Erdos3.DilationBudget.exists_full_bound line 101