OAI/Analysis/HardSphere/Geometry/SparseChecks.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.HardSphere.Comparison.Edge line 19
2. def OAI.HardSphere.Comparison.sparseReference line 21
3. def OAI.HardSphere.Comparison.sparseProposal line 24
4. lemma OAI.HardSphere.Comparison.sparse_primary line 28
5. lemma OAI.HardSphere.Comparison.sparse_outside line 41
6. lemma OAI.HardSphere.Comparison.pair_subset_one line 59
7. lemma OAI.HardSphere.Comparison.sparse_reference_separated line 79
8. lemma OAI.HardSphere.Comparison.sparse_proposal_separated line 87
9. lemma OAI.HardSphere.Groups.confined_far_avoid line 103
10. lemma OAI.HardSphere.Groups.incident_centers_close line 114