OAI/Analysis/HardSphere/Geometry/RoundBox.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HardSphere.Lattice.double_avoiding_step line 13
2. lemma OAI.HardSphere.Lattice.double_avoidingReach line 29
3. def OAI.HardSphere.Lattice.roundBox line 37
4. lemma OAI.HardSphere.Lattice.roundBox_nonempty line 39
5. lemma OAI.HardSphere.Lattice.roundBox_NNConnected line 44
6. lemma OAI.HardSphere.Lattice.roundBox_overlap line 54
7. lemma OAI.HardSphere.Lattice.nearestStep_starBound line 66
8. lemma OAI.HardSphere.Lattice.roundBox_avoids line 74
9. lemma OAI.HardSphere.Lattice.round_nearest_reach line 83
10. lemma OAI.HardSphere.Lattice.round_avoidingReach line 91
11. lemma OAI.HardSphere.Lattice.mem_round_double line 105
12. lemma OAI.HardSphere.Lattice.round_component_exterior line 108
13. lemma OAI.HardSphere.Lattice.round_boundary_shell line 115
14. lemma OAI.HardSphere.Lattice.withinReach_first_entry line 132
15. lemma OAI.HardSphere.Lattice.shell_covered_by_boundary line 143
16. lemma OAI.HardSphere.Lattice.round_boundary_reach line 175
17. theorem OAI.HardSphere.Lattice.exteriorShell_NNConnected line 191
18. lemma OAI.HardSphere.Lattice.nearestStep_ne line 200
19. lemma OAI.HardSphere.Lattice.nearestStep_star line 205
20. lemma OAI.HardSphere.Lattice.mem_fill_of_mem line 208
21. def OAI.HardSphere.Lattice.detourRegion line 211
22. def OAI.HardSphere.Lattice.goodDetourRegion line 214
23. theorem OAI.HardSphere.Lattice.good_detour_reach line 217
24. def OAI.HardSphere.Lattice.detourVertices line 276
25. lemma OAI.HardSphere.Lattice.mem_detourVertices line 279
26. lemma OAI.HardSphere.Lattice.detourVertices_card_le line 284
27. def OAI.HardSphere.Lattice.nearestGraph line 297
28. def OAI.HardSphere.Lattice.restrictedNearestGraph line 302
29. lemma OAI.HardSphere.Lattice.withinReach_simple_path line 307
30. theorem OAI.HardSphere.Lattice.simple_good_detour line 338