OAI/Analysis/HardSphere/Geometry/JoinConfiguration.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HardSphere.joinConfiguration line 16
  2. def OAI.HardSphere.splitConfiguration line 20
  3. lemma OAI.HardSphere.joinConfiguration_continuous line 24
  4. lemma OAI.HardSphere.splitConfiguration_continuous line 34
  5. lemma OAI.HardSphere.split_joinConfiguration line 37
  6. lemma OAI.HardSphere.join_splitConfiguration line 42
  7. lemma OAI.HardSphere.joinConfiguration_preserving line 47
  8. lemma OAI.HardSphere.splitConfiguration_preserving line 59
  9. def OAI.HardSphere.joinConfigurationPath line 68
  10. def OAI.HardSphere.splitConfigurationPath line 73
  11. lemma OAI.HardSphere.joinConfigurationPath_continuous line 78
  12. lemma OAI.HardSphere.splitConfigurationPath_continuous line 85
  13. lemma OAI.HardSphere.split_joinConfigurationPath line 95
  14. lemma OAI.HardSphere.join_splitConfigurationPath line 100
  15. lemma OAI.HardSphere.measurePreserving_shuffle line 107
  16. def OAI.HardSphere.directionSumEquiv line 120
  17. def OAI.HardSphere.joinCoordinatePaths line 124
  18. lemma OAI.HardSphere.joinCoordinatePaths_preserving line 127
  19. lemma OAI.HardSphere.freeTrajectory_join line 138
  20. lemma OAI.HardSphere.joinConfigurationPath_preserving line 146
  21. lemma OAI.HardSphere.splitConfigurationPath_preserving line 162
  22. lemma OAI.HardSphere.staysAllowed_join_subset_bath line 171