OAI/Analysis/HardSphere/Conditioning/ReverseConfigurationPath.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HardSphere.reverseConfigurationPath line 19
  2. lemma OAI.HardSphere.reverseConfigurationPath_continuous line 22
  3. lemma OAI.HardSphere.reverseConfigurationPath_apply line 28
  4. lemma OAI.HardSphere.reverseConfigurationPath_reverse line 32
  5. lemma OAI.HardSphere.staysAllowed_reverse line 38
  6. lemma OAI.HardSphere.coordinateReverse_preserving line 48
  7. lemma OAI.HardSphere.reverse_freeTrajectory line 56
  8. lemma OAI.HardSphere.reverse_freePath_preserving line 68
  9. lemma OAI.HardSphere.reverse_killedPath_preserving line 102
  10. def OAI.HardSphere.reversePathEquiv line 111
  11. lemma OAI.HardSphere.killedTransition_selfAdjoint line 119