OAI/Combinatorics/Progressions/Estimates/SiteTwistCommonModulus.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.finite_site_product_expansion line 15
  2. theorem OAI.Erdos3.finite_site_product_coefficient_norm line 24
  3. theorem OAI.Erdos3.finite_site_product_coefficient_norm_le line 28
  4. theorem OAI.Erdos3.finite_site_axis_product_lipschitz line 35
  5. theorem OAI.Erdos3.finite_site_product_approximation line 48
  6. structure OAI.Erdos3.ScalarSiteExpansion line 73
  7. structure OAI.Erdos3.ScalarSiteExpansion.Bounds line 86
  8. def OAI.Erdos3.ScalarSiteExpansion.eval line 95
  9. def OAI.Erdos3.ScalarSiteExpansion.integerEval line 98
  10. theorem OAI.Erdos3.ScalarSiteExpansion.eval_norm_le line 101
  11. theorem OAI.Erdos3.ScalarSiteExpansion.Bounds.mono line 126
  12. def OAI.Erdos3.ScalarSiteExpansion.rescale line 145
  13. theorem OAI.Erdos3.ScalarSiteExpansion.rescale_eval line 151
  14. theorem OAI.Erdos3.ScalarSiteExpansion.rescale_bounds line 157
  15. theorem OAI.Erdos3.ScalarSiteExpansion.rescale_integerEval line 177
  16. theorem OAI.Erdos3.ScalarSiteExpansion.rescale_integer_error line 189
  17. def OAI.Erdos3.siteFamilyCoefficient line 227
  18. def OAI.Erdos3.siteFamilyFactor line 230
  19. def OAI.Erdos3.siteFamilyEval line 234
  20. theorem OAI.Erdos3.siteFamilyEval_eq line 238
  21. theorem OAI.Erdos3.siteFamily_card_le line 249
  22. theorem OAI.Erdos3.siteFamily_coefficient_le line 255
  23. theorem OAI.Erdos3.siteFamilyFactor_bounds line 261
  24. theorem OAI.Erdos3.siteFamilyFactor_support line 270
  25. theorem OAI.Erdos3.siteFamily_approximation line 276
  26. def OAI.Erdos3.commonSitePeriod line 298
  27. theorem OAI.Erdos3.commonSitePeriod_dvd line 300
  28. theorem OAI.Erdos3.commonSitePeriod_pos line 304
  29. theorem OAI.Erdos3.commonSitePeriod_le_pow line 309
  30. def OAI.Erdos3.scaledSiteCoordinates line 333
  31. theorem OAI.Erdos3.scaledSiteCoordinates_lipschitz line 336
  32. def OAI.Erdos3.scaledSiteFamilyFactor line 350
  33. theorem OAI.Erdos3.scaledSiteFamilyFactor_bounds line 354
  34. theorem OAI.Erdos3.scaledSiteFamilyFactor_support line 364
  35. theorem OAI.Erdos3.scaledSiteFamilyFactor_eval line 378
  36. theorem OAI.Erdos3.ScalarSiteExpansion.eval_eq_zero_of_large line 396
  37. def OAI.Erdos3.reconstructedSiteEval line 406
  38. theorem OAI.Erdos3.reconstructedSiteEval_zero_off_window line 410
  39. def OAI.Erdos3.ScalarSiteExpansion.atCeilScale line 445
  40. theorem OAI.Erdos3.ScalarSiteExpansion.atCeilScale_bounds line 449
  41. theorem OAI.Erdos3.ScalarSiteExpansion.atCeilScale_integer_error line 474
  42. def OAI.Erdos3.siteTwistCommonModulus line 497
  43. theorem OAI.Erdos3.siteTwistCommonModulus_pos line 500
  44. theorem OAI.Erdos3.siteTwistCommonModulus_spatial_dvd line 506
  45. theorem OAI.Erdos3.siteTwistCommonModulus_grid_dvd line 512
  46. theorem OAI.Erdos3.siteTwistCommonModulus_ideal_dvd line 518
  47. theorem OAI.Erdos3.siteTwistCommonModulus_exp_bound line 522
  48. def OAI.Erdos3.BooleanCubeKernel.physicalResidueSpatialMaskMod line 548
  49. theorem OAI.Erdos3.BooleanCubeKernel.physicalResidueSpatialMaskMod_eval line 555
  50. theorem OAI.Erdos3.BooleanCubeKernel.physicalResidueSpatialMaskMod_norm line 561