OAI/Analysis/HardSphere/Bridges/GroundBridge.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HardSphere.preserving_weighted line 16
  2. abbrev OAI.HardSphere.BridgeEndpoints line 25
  3. def OAI.HardSphere.bridgeEndpointBase line 27
  4. def OAI.HardSphere.endpointBridgePath line 30
  5. lemma OAI.HardSphere.endpointBridgePath_continuous line 34
  6. lemma OAI.HardSphere.endpointBridgePath_preserving line 39
  7. def OAI.HardSphere.bridgeEnd line 51
  8. lemma OAI.HardSphere.bridgeEnd_continuous line 53
  9. def OAI.HardSphere.endpointWeight line 57
  10. lemma OAI.HardSphere.endpointWeight_measurable line 59
  11. lemma OAI.HardSphere.endpointBridge_weight line 64
  12. def OAI.HardSphere.endpointInteraction line 81
  13. lemma OAI.HardSphere.endpointInteraction_measurable line 83
  14. def OAI.HardSphere.endpointWeightedBase line 86
  15. lemma OAI.HardSphere.genuine_ground_bridge line 89