OAI/Geometry/TranslativeCovering/Periodization.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.TranslativeCovering.isCompact_cube line 106
  2. lemma OAI.TranslativeCovering.exists_cube_superset line 117
  3. def OAI.TranslativeCovering.cubePeriod line 124
  4. def OAI.TranslativeCovering.repeatCube line 127
  5. lemma OAI.TranslativeCovering.cube_cover_mod_period line 130
  6. lemma OAI.TranslativeCovering.restrict_cover_window line 146
  7. lemma OAI.TranslativeCovering.periodize_cover line 159
  8. lemma OAI.TranslativeCovering.finite_cover_window line 168
  9. structure OAI.TranslativeCovering.CubicCover line 183
  10. def OAI.TranslativeCovering.cubicCenterInfimum line 189
  11. lemma OAI.TranslativeCovering.cubicCenterInfimum_le_window line 193
  12. lemma OAI.TranslativeCovering.cubicCenterInfimum_le_upperIntensity line 207
  13. lemma OAI.TranslativeCovering.cubic_density_le_thetaT line 252
  14. def OAI.TranslativeCovering.integerGrid line 259
  15. lemma OAI.TranslativeCovering.card_integerGrid line 262
  16. lemma OAI.TranslativeCovering.repeatCube_window_subset line 267
  17. lemma OAI.TranslativeCovering.repeatCube_window_finite line 290
  18. lemma OAI.TranslativeCovering.repeatCube_locallyFinite line 295
  19. lemma OAI.TranslativeCovering.repeatCube_count_le line 303
  20. lemma OAI.TranslativeCovering.repeatCube_count_le_real line 311
  21. lemma OAI.TranslativeCovering.upperIntensity_repeatCube_le line 324
  22. theorem OAI.TranslativeCovering.thetaT_eq_cubic line 360
  23. theorem OAI.TranslativeCovering.periodization line 374