OAI/Analysis/HardSphere/Cutoffs/PathDiameter.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.HardSphere.PathCutoff.intervalTime line 15
  2. lemma OAI.HardSphere.PathCutoff.intervalTime_continuous line 23
  3. lemma OAI.HardSphere.PathCutoff.intervalTime_zero line 27
  4. lemma OAI.HardSphere.PathCutoff.intervalTime_one line 30
  5. def OAI.HardSphere.PathCutoff.diameterMap line 34
  6. def OAI.HardSphere.PathCutoff.intervalDiameter line 40
  7. lemma OAI.HardSphere.PathCutoff.diameterMap_continuous line 43
  8. lemma OAI.HardSphere.PathCutoff.intervalDiameter_continuous line 52
  9. lemma OAI.HardSphere.PathCutoff.intervalDiameter_nonneg line 55
  10. lemma OAI.HardSphere.PathCutoff.intervalDistance_le line 58
  11. lemma OAI.HardSphere.PathCutoff.intervalDiameter_le line 62
  12. lemma OAI.HardSphere.PathCutoff.intervalTime_reverse line 71
  13. lemma OAI.HardSphere.PathCutoff.intervalDiameter_reverse line 77
  14. def OAI.HardSphere.PathCutoff.meshTime line 102
  15. lemma OAI.HardSphere.PathCutoff.meshTime_continuous line 109
  16. def OAI.HardSphere.PathCutoff.meshSegment line 113
  17. lemma OAI.HardSphere.PathCutoff.meshSegment_continuous line 116
  18. lemma OAI.HardSphere.PathCutoff.meshSegment_one line 122
  19. lemma OAI.HardSphere.PathCutoff.mesh_firstTime line 131
  20. lemma OAI.HardSphere.PathCutoff.mesh_nextTime line 137
  21. lemma OAI.HardSphere.PathCutoff.meshSegment_first line 146
  22. lemma OAI.HardSphere.PathCutoff.meshSegment_next line 151
  23. lemma OAI.HardSphere.PathCutoff.meshTime_reverse line 156
  24. lemma OAI.HardSphere.PathCutoff.meshSegment_reverse line 169
  25. lemma OAI.HardSphere.PathCutoff.mesh_sum_reverse line 174