OAI/Analysis/HardSphere/Geometry/DiscreteTorus.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.HardSphere.Lattice.DiscreteTorus line 12
2. def OAI.HardSphere.Lattice.torusProjection line 14
3. def OAI.HardSphere.Lattice.rangeStep line 16
4. def OAI.HardSphere.Lattice.torusRangeStep line 18
5. lemma OAI.HardSphere.Lattice.rangeStep_symm line 21
6. lemma OAI.HardSphere.Lattice.torusRangeStep_symm line 24
7. def OAI.HardSphere.Lattice.forbiddenCuts line 31
8. lemma OAI.HardSphere.Lattice.forbiddenCuts_card line 34
9. lemma OAI.HardSphere.Lattice.exists_vacant_cut line 45
10. lemma OAI.HardSphere.Lattice.cut_coordinate_bound line 54
11. def OAI.HardSphere.Lattice.cutLift line 67
12. lemma OAI.HardSphere.Lattice.cutLift_projection line 70
13. lemma OAI.HardSphere.Lattice.small_multiple_zero line 76
14. lemma OAI.HardSphere.Lattice.cutLift_edge line 81
15. theorem OAI.HardSphere.Lattice.small_set_lift line 107
16. lemma OAI.HardSphere.Lattice.connected_coordinate_span line 115
17. def OAI.HardSphere.Lattice.torusRangeGraph line 134
18. def OAI.HardSphere.Lattice.periodicLift line 139
19. lemma OAI.HardSphere.Lattice.short_projection_ne line 143
20. lemma OAI.HardSphere.Lattice.rangeStep_projection line 154
21. lemma OAI.HardSphere.Lattice.lift_offset_step line 160
22. lemma OAI.HardSphere.Lattice.lift_offset_reach line 183
23. lemma OAI.HardSphere.Lattice.translated_projection line 194
24. lemma OAI.HardSphere.Lattice.rangeStep_translate line 205
25. lemma OAI.HardSphere.Lattice.translated_reach line 210
26. theorem OAI.HardSphere.Lattice.small_periodic_lifts line 237