OAI/Analysis/HardSphere/Cutoffs/PathLift.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.HardSphere.PathCutoff.EuclideanPath line 16
  2. def OAI.HardSphere.PathCutoff.IsPathLift line 17
  3. lemma OAI.HardSphere.PathCutoff.exists_pathLift line 20
  4. lemma OAI.HardSphere.PathCutoff.liftDiff_coe line 30
  5. lemma OAI.HardSphere.PathCutoff.liftDiff_lt_half_period line 35
  6. lemma OAI.HardSphere.PathCutoff.liftDiff_norm_eq line 53
  7. def OAI.HardSphere.PathCutoff.liftedDiameterMap line 63
  8. def OAI.HardSphere.PathCutoff.liftedDiameter line 71
  9. lemma OAI.HardSphere.PathCutoff.liftedDiameter_eq line 73
  10. lemma OAI.HardSphere.PathCutoff.intervalDiameter_le_lifted line 96
  11. lemma OAI.HardSphere.PathCutoff.interval_small_iff_lifted_small line 114
  12. lemma OAI.HardSphere.PathCutoff.intervalTime_assoc line 123
  13. lemma OAI.HardSphere.PathCutoff.meshSegment_lift line 129
  14. lemma OAI.HardSphere.PathCutoff.diameterRatio_reverse line 148
  15. lemma OAI.HardSphere.PathCutoff.meshRegular_reverse line 154
  16. def OAI.HardSphere.PathCutoff.EndpointRegular line 165
  17. def OAI.HardSphere.PathCutoff.Regular line 168
  18. lemma OAI.HardSphere.PathCutoff.regular_measurable line 171
  19. lemma OAI.HardSphere.PathCutoff.endpointRegular_reverse line 179
  20. lemma OAI.HardSphere.PathCutoff.regular_reverse line 185
  21. lemma OAI.HardSphere.PathCutoff.mesh_lift_diameter line 189
  22. lemma OAI.HardSphere.PathCutoff.regular_lifted_iff line 197
  23. lemma OAI.HardSphere.PathCutoff.interval_prefix line 221
  24. lemma OAI.HardSphere.PathCutoff.interval_suffix line 233