OAI/Combinatorics/Progressions/Geometry/SpatialSiteShift.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.spatialStarDensity line 13
  2. theorem OAI.Erdos3.spatialStarDensity_lipschitz line 16
  3. theorem OAI.Erdos3.spatialStarDensity_bound line 23
  4. def OAI.Erdos3.spatialSiteApprox line 27
  5. theorem OAI.Erdos3.spatialSiteApprox_error line 34
  6. theorem OAI.Erdos3.spatialSiteApprox_coefficient_sum line 51
  7. def OAI.Erdos3.spatialSiteRadius line 63
  8. theorem OAI.Erdos3.spatialSiteRadius_pos line 65
  9. theorem OAI.Erdos3.spatialSiteRadius_error line 68
  10. theorem OAI.Erdos3.intervalTensorApprox_zero_outside line 86
  11. theorem OAI.Erdos3.spatialSiteApprox_zero_outside line 108
  12. theorem OAI.Erdos3.intervalTensorApprox_norm_le line 134
  13. theorem OAI.Erdos3.maskedIntegerImageDensity_abs_le line 148
  14. theorem OAI.Erdos3.spatialSiteApprox_norm_le line 160
  15. theorem OAI.Erdos3.norm_weighted_complex_mean_sub_le line 183
  16. theorem OAI.Erdos3.norm_site_family_replacement line 204
  17. theorem OAI.Erdos3.norm_fiber_site_replacement line 218
  18. abbrev OAI.Erdos3.SpatialSiteLabel line 247
  19. def OAI.Erdos3.spatialSiteCoefficient line 250
  20. theorem OAI.Erdos3.spatialSiteApprox_sum line 256
  21. theorem OAI.Erdos3.spatialSiteCoefficient_sum_bound line 265
  22. theorem OAI.Erdos3.vectorSpatialSiteExpansion line 274
  23. theorem OAI.Erdos3.vectorSpatialSiteCoefficient_sum_bound line 287
  24. theorem OAI.Erdos3.vectorSpatialSiteLabel_card line 302
  25. theorem OAI.Erdos3.spatialSiteTerm_zero_outside line 318
  26. theorem OAI.Erdos3.vectorSpatialSiteApprox_error line 360
  27. theorem OAI.Erdos3.spatialSiteApprox_remesh line 413
  28. theorem OAI.Erdos3.vectorSpatialSiteApprox_remesh line 439
  29. theorem OAI.Erdos3.weightedSpatialSiteApprox_remesh line 467
  30. theorem OAI.Erdos3.spatialSiteApprox_shift line 501
  31. theorem OAI.Erdos3.vectorSpatialSiteApprox_shift line 536