OAI/Combinatorics/Progressions/Estimates/BufferedSiteExpansion.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.lipschitz_mul_star_of_bounds line 14
  2. theorem OAI.Erdos3.lipschitz_mul_of_bounds line 48
  3. theorem OAI.Erdos3.bounded_lipschitz_finset_prod line 60
  4. theorem OAI.Erdos3.bounded_lipschitz_fintype_prod line 89
  5. theorem OAI.Erdos3.ambient_nsmul_lipschitz line 106
  6. theorem OAI.Erdos3.ambient_pair_lipschitz line 113
  7. theorem OAI.Erdos3.finite_lipschitz_linear_combination line 141
  8. theorem OAI.Erdos3.finiteSiteExpansion_product line 173
  9. theorem OAI.Erdos3.finiteSiteExpansion_product_mass line 185
  10. theorem OAI.Erdos3.finiteSiteExpansion_product_factor line 190
  11. theorem OAI.Erdos3.finiteNestedSiteExpansion_transport line 205
  12. theorem OAI.Erdos3.siteBudget_of_rowBudget line 214
  13. theorem OAI.Erdos3.finiteNestedSiteExpansion_mass line 219
  14. theorem OAI.Erdos3.finiteNestedSiteExpansion_product_functions line 225
  15. theorem OAI.Erdos3.lipschitz_real_mul_of_bounds line 258
  16. theorem OAI.Erdos3.bounded_lipschitz_real_prod line 280
  17. theorem OAI.Erdos3.siteFactorTensor_identity line 309
  18. theorem OAI.Erdos3.siteFactorTensor_coefficient_sum line 319
  19. theorem OAI.Erdos3.siteFactorTensor_coefficient_bound line 325
  20. theorem OAI.Erdos3.siteFactorTensor_factor_bound line 332
  21. theorem OAI.Erdos3.siteFactorTensor_factor_lipschitz line 337
  22. theorem OAI.Erdos3.finiteSiteExpansion_test_expect line 358
  23. def OAI.Erdos3.bufferedSiteFactor line 386
  24. theorem OAI.Erdos3.bufferedSiteExpansion_identity line 390
  25. theorem OAI.Erdos3.bufferedSiteFactor_bound line 401
  26. theorem OAI.Erdos3.bufferedSiteFactor_lipschitz line 410
  27. theorem OAI.Erdos3.bufferedSiteExpansion_error line 421