OAI/Analysis/HardSphere/Bridges/ReferenceHit.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HardSphere.Bridge.earlyTorusHit_measurable line 18
2. lemma OAI.HardSphere.Bridge.leg_reverse line 50
3. lemma OAI.HardSphere.Bridge.project_leg_reverse line 58
4. lemma OAI.HardSphere.Bridge.leg_endpoints_ae line 66
5. lemma OAI.HardSphere.Bridge.reference_collision line 73
6. lemma OAI.HardSphere.Bridge.individual_normalizer_lower line 142
7. lemma OAI.HardSphere.Bridge.normalized_collision_le line 169