OAI/Analysis/HardSphere/Bridges/NormalizedPrefix.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HardSphere.Wiener.normalizedPrefix line 18
  2. def OAI.HardSphere.Wiener.normalizedSuffix line 21
  3. lemma OAI.HardSphere.Wiener.normalized_split_preserving line 24
  4. def OAI.HardSphere.splitTime line 48
  5. lemma OAI.HardSphere.splitTime_pos line 51
  6. lemma OAI.HardSphere.splitTime_lt_one line 54
  7. lemma OAI.HardSphere.sqrt_split_left line 57
  8. lemma OAI.HardSphere.sqrt_split_right line 66
  9. def OAI.HardSphere.configurationPrefix line 76
  10. def OAI.HardSphere.configurationSuffix line 79
  11. lemma OAI.HardSphere.configurationPrefix_continuous line 82
  12. lemma OAI.HardSphere.configurationSuffix_continuous line 88
  13. lemma OAI.HardSphere.coordinateSplit_preserving line 94
  14. lemma OAI.HardSphere.prefix_freeTrajectory line 110
  15. lemma OAI.HardSphere.suffix_freeTrajectory line 119
  16. lemma OAI.HardSphere.prefixTime_one line 131
  17. lemma OAI.HardSphere.prefixTime_zero line 135
  18. lemma OAI.HardSphere.suffixTime_zero line 139
  19. lemma OAI.HardSphere.suffixTime_one line 143
  20. lemma OAI.HardSphere.staysAllowed_split line 147
  21. lemma OAI.HardSphere.split_freePathLaw line 176