OAI/Combinatorics/Progressions/Dynamics/VectorSiteBudget.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.siteTermCount line 9
  2. theorem OAI.Erdos3.spatialSiteRadius_inverse_le_exp line 13
  3. theorem OAI.Erdos3.intervalSiteCount_bound line 34
  4. theorem OAI.Erdos3.intervalSiteCount_le_exp line 40
  5. theorem OAI.Erdos3.intervalSiteLipschitz_le_exp line 57
  6. theorem OAI.Erdos3.siteCoefficientAllowance_le_exp line 72
  7. theorem OAI.Erdos3.exists_grouped_site_approximation line 94
  8. def OAI.Erdos3.vectorSpatialAccuracy line 150
  9. theorem OAI.Erdos3.vectorSpatialAccuracy_pos line 153
  10. theorem OAI.Erdos3.vectorSpatialAccuracy_le line 156
  11. theorem OAI.Erdos3.vectorSpatialAccuracy_error line 162
  12. theorem OAI.Erdos3.vectorSpatialSiteError_le line 170
  13. theorem OAI.Erdos3.vectorSpatialAccuracy_inverse_le_exp line 193
  14. theorem OAI.Erdos3.vectorSiteAllowance_le_exp line 209
  15. theorem OAI.Erdos3.vectorSiteLipschitz_le_exp line 213