OAI/Analysis/HardSphere/Collisions/InsertionCount.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HardSphere.closeLabels_cons line 20
2. lemma OAI.HardSphere.closeLabels_insert_le line 30
3. def OAI.HardSphere.insertionCount line 47
4. lemma OAI.HardSphere.insertionCount_zero line 50
5. lemma OAI.HardSphere.insertionCount_succ line 53
6. lemma OAI.HardSphere.insertionCount_mono line 57
7. lemma OAI.HardSphere.local_insertion_iterated line 64