OAI/Analysis/HardSphere/Geometry/StarGraph.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HardSphere.Lattice.starGraph line 13
2. def OAI.HardSphere.Lattice.restrictedStarGraph line 18
3. lemma OAI.HardSphere.Lattice.withinReach_star_path line 23
4. lemma OAI.HardSphere.Lattice.withinReach_star_first_entry line 53
5. theorem OAI.HardSphere.Lattice.star_first_exit line 65
6. lemma OAI.HardSphere.Lattice.star_path_span line 96
7. lemma OAI.HardSphere.BathSlice.local_projection_injective line 116
8. lemma OAI.HardSphere.BathSlice.card_witness_sites_le line 135