OAI/Analysis/HardSphere/Geometry/PathPermutation.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HardSphere.permuteConfiguration_continuous line 15
  2. def OAI.HardSphere.permuteConfigurationPath line 20
  3. lemma OAI.HardSphere.permuteConfigurationPath_continuous line 24
  4. def OAI.HardSphere.permuteCoordinatePaths line 30
  5. lemma OAI.HardSphere.permuteCoordinatePaths_preserving line 33
  6. lemma OAI.HardSphere.freeTrajectory_permute line 42
  7. lemma OAI.HardSphere.permute_freePath_preserving line 47
  8. lemma OAI.HardSphere.permute_staysAllowed line 57
  9. lemma OAI.HardSphere.permute_killedPath_preserving line 67
  10. lemma OAI.HardSphere.measurePreserving_weighted_ae_invariant line 73
  11. lemma OAI.HardSphere.groundPositionLaw_permute line 89
  12. lemma OAI.HardSphere.groundPathLaw_permute line 98