OAI/GroupTheory/SimpleAmenable/Arithmetic/LatticeCounting.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SimpleAmenable.embeddingBox line 12
  2. theorem OAI.SimpleAmenable.embeddingBox_floor_injective line 15
  3. theorem OAI.SimpleAmenable.embeddingBox_floor_mapsTo line 36
  4. theorem OAI.SimpleAmenable.embeddingBox_finite line 43
  5. theorem OAI.SimpleAmenable.embeddingBox_card_le line 48
  6. def OAI.SimpleAmenable.dividedEmbeddingBox line 71
  7. theorem OAI.SimpleAmenable.dividedEmbeddingBox_eq line 75
  8. theorem OAI.SimpleAmenable.dividedEmbeddingBox_finite line 83
  9. theorem OAI.SimpleAmenable.dividedEmbeddingBox_card_le line 88
  10. theorem OAI.SimpleAmenable.pairedEmbeddingBox_card_le line 95
  11. lemma OAI.SimpleAmenable.floor_error line 126
  12. theorem OAI.SimpleAmenable.quadratic_lattice_cover line 130
  13. theorem OAI.SimpleAmenable.scaled_quadratic_lattice_cover line 181
  14. theorem OAI.SimpleAmenable.endpoint_separation line 216
  15. theorem OAI.SimpleAmenable.coordinate_window_net line 238