OAI/Combinatorics/Progressions/Estimates/GroupedSiteTensor.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.vectorIntervalSiteWeight line 11
  2. theorem OAI.Erdos3.vectorIntervalSiteWeight_bound line 15
  3. theorem OAI.Erdos3.vectorIntervalSiteWeight_lipschitz line 24
  4. def OAI.Erdos3.vectorResidueSiteWeight line 37
  5. theorem OAI.Erdos3.vectorResidueSiteWeight_eq line 41
  6. theorem OAI.Erdos3.vectorResidueSiteWeight_bound line 51
  7. def OAI.Erdos3.groupedSiteCoefficient line 72
  8. def OAI.Erdos3.groupedSiteFactor line 76
  9. def OAI.Erdos3.groupedSiteApprox line 80
  10. theorem OAI.Erdos3.siteCurry_lipschitz line 86
  11. theorem OAI.Erdos3.groupedSiteApprox_eq_interval line 97
  12. theorem OAI.Erdos3.groupedSiteApprox_error line 109
  13. theorem OAI.Erdos3.groupedSiteCoefficient_sum line 119
  14. theorem OAI.Erdos3.groupedSiteFactor_bound line 129
  15. theorem OAI.Erdos3.groupedSiteFactor_lipschitz line 135