OAI/Geometry/TranslativeCovering/LocalizationRounding.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.LocalizationRounding.Space line 11
  2. def OAI.LocalizationRounding.weight line 12
  3. lemma OAI.LocalizationRounding.truncated_square line 14
  4. lemma OAI.LocalizationRounding.weight_lipschitz line 39
  5. def OAI.LocalizationRounding.rounded line 51
  6. lemma OAI.LocalizationRounding.rounded_coord line 54
  7. lemma OAI.LocalizationRounding.rounding_error line 67
  8. lemma OAI.LocalizationRounding.residual_error line 80
  9. lemma OAI.LocalizationRounding.norm_buffer line 87
  10. lemma OAI.LocalizationRounding.slab_buffer line 93
  11. lemma OAI.LocalizationRounding.weight_transfer line 103
  12. def OAI.LocalizationRounding.latticePoint line 113
  13. def OAI.LocalizationRounding.integerBox line 115
  14. def OAI.LocalizationRounding.alphabet line 117
  15. lemma OAI.LocalizationRounding.latticePoint_mem_box line 121
  16. lemma OAI.LocalizationRounding.mem_alphabet line 136
  17. lemma OAI.LocalizationRounding.rounded_mem_alphabet line 147
  18. lemma OAI.LocalizationRounding.alphabet_card line 157
  19. abbrev OAI.LocalizationRounding.BoundedLists line 180
  20. lemma OAI.LocalizationRounding.boundedLists_card line 183