OAI/Analysis/HardSphere/Geometry/TorusBall.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HardSphere.Lattice.shortest_representative line 12
2. lemma OAI.HardSphere.Lattice.projection_near line 23
3. lemma OAI.HardSphere.Lattice.nominal_index_bound line 30
4. lemma OAI.HardSphere.Lattice.nominal_equal_index line 47
5. def OAI.HardSphere.Lattice.torusBall line 63
6. lemma OAI.HardSphere.Lattice.mem_torusBall line 66
7. theorem OAI.HardSphere.Lattice.nominal_encounter_bound line 69
8. lemma OAI.HardSphere.Lattice.candidate_nonempty line 106
9. lemma OAI.HardSphere.Lattice.candidate_reach line 110
10. lemma OAI.HardSphere.Lattice.candidate_diameter line 115
11. lemma OAI.HardSphere.Lattice.candidate_contact_root line 131
12. theorem OAI.HardSphere.Lattice.contact_candidates_card line 160