OAI/Analysis/HardSphere/Geometry/MicroPeriod.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HardSphere.BathSlice.not_small_has_exit line 16
2. theorem OAI.HardSphere.BathSlice.large_component_witnesses line 34
3. def OAI.HardSphere.BathSlice.microPeriod line 52
4. def OAI.HardSphere.BathSlice.microMesh line 53
5. lemma OAI.HardSphere.BathSlice.microPeriod_pos line 55
6. lemma OAI.HardSphere.BathSlice.microMesh_bounds line 58