OAI/Analysis/HardSphere/Bridges/PhaseBridge.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.HardSphere.liftedBridgePath line 13
2. def OAI.HardSphere.projectedBridgePath line 17
3. lemma OAI.HardSphere.reconstructed_bridge_eq line 21
4. lemma OAI.HardSphere.projectedBridgePath_endpoints line 36
5. lemma OAI.HardSphere.killed_ae_lifted_bridges line 48
6. lemma OAI.HardSphere.exists_bridge_bounded_positive line 77
7. lemma OAI.HardSphere.liftedBridge_distance line 90
8. lemma OAI.HardSphere.projectedBridge_stays_of_bounded line 107
9. lemma OAI.HardSphere.killed_ae_local_pairs line 123