OAI/Combinatorics/Progressions/Polynomial/LocalizationPolynomialScales.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.localizationRadius line 9
  2. def OAI.Erdos3.localizationMesh line 10
  3. def OAI.Erdos3.localizationLengthBudget line 11
  4. theorem OAI.Erdos3.localizationRadius_pos line 13
  5. theorem OAI.Erdos3.localizationMesh_pos line 16
  6. theorem OAI.Erdos3.localizationRadius_le_one line 19
  7. theorem OAI.Erdos3.localizationMesh_le_one line 26
  8. theorem OAI.Erdos3.localizationRadius_scale line 33
  9. theorem OAI.Erdos3.localizationMesh_scale line 39
  10. theorem OAI.Erdos3.localizationMesh_length line 46
  11. theorem OAI.Erdos3.localizationRadius_length line 53
  12. theorem OAI.Erdos3.localizationMesh_margin line 60
  13. theorem OAI.Erdos3.localizationLengthBudget_ge_square line 73
  14. theorem OAI.Erdos3.localization_inverse_length_error line 85