OAI/Analysis/HardSphere/Paths/NearPotential.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HardSphere.DyadicSkeleton.orderedEncounterConstant_one_le line 12
  2. def OAI.HardSphere.DyadicSkeleton.nearPotential line 16
  3. lemma OAI.HardSphere.DyadicSkeleton.nearPotential_nonneg line 18
  4. lemma OAI.HardSphere.DyadicSkeleton.nearPotential_le_one line 20
  5. lemma OAI.HardSphere.DyadicSkeleton.nearPotential_cast line 24
  6. lemma OAI.HardSphere.DyadicSkeleton.measurable_nearPotential line 27
  7. def OAI.HardSphere.DyadicSkeleton.singleRadiusWeights line 30
  8. lemma OAI.HardSphere.DyadicSkeleton.singleRadiusWeights_envelope line 31
  9. lemma OAI.HardSphere.DyadicSkeleton.singleRadiusWeights_activity line 35
  10. def OAI.HardSphere.DyadicSkeleton.hitConstant line 40
  11. lemma OAI.HardSphere.DyadicSkeleton.hitConstant_pos line 41
  12. lemma OAI.HardSphere.DyadicSkeleton.hitConstant_le_one line 44
  13. lemma OAI.HardSphere.DyadicSkeleton.same_time_hit_moment line 50
  14. def OAI.HardSphere.DyadicSkeleton.transverseDistance line 85
  15. lemma OAI.HardSphere.DyadicSkeleton.transverseDistance_nonneg line 87
  16. lemma OAI.HardSphere.DyadicSkeleton.measurable_transverseDistance line 89
  17. lemma OAI.HardSphere.DyadicSkeleton.nearTest_eq_one line 91
  18. def OAI.HardSphere.DyadicSkeleton.softPotential line 96
  19. lemma OAI.HardSphere.DyadicSkeleton.softPotential_nonneg line 98
  20. lemma OAI.HardSphere.DyadicSkeleton.softPotential_le_one line 100
  21. lemma OAI.HardSphere.DyadicSkeleton.measurable_softPotential line 104
  22. def OAI.HardSphere.DyadicSkeleton.softWeights line 107
  23. lemma OAI.HardSphere.DyadicSkeleton.softPotential_envelope line 108
  24. lemma OAI.HardSphere.DyadicSkeleton.soft_activity_ne_top line 123
  25. lemma OAI.HardSphere.DyadicSkeleton.same_time_soft_moment line 149
  26. def OAI.HardSphere.DyadicSkeleton.twoCopyDistance line 195
  27. lemma OAI.HardSphere.DyadicSkeleton.measurable_twoCopyDistance line 198
  28. lemma OAI.HardSphere.DyadicSkeleton.measurable_twoCopyNear line 206
  29. lemma OAI.HardSphere.DyadicSkeleton.two_copy_hit_moment line 219
  30. lemma OAI.HardSphere.DyadicSkeleton.two_copy_soft_moment line 234
  31. lemma OAI.HardSphere.DyadicSkeleton.position_lipschitz line 247
  32. lemma OAI.HardSphere.DyadicSkeleton.position_abs_le line 267
  33. lemma OAI.HardSphere.DyadicSkeleton.fold_time_lipschitz line 271
  34. abbrev OAI.HardSphere.DyadicSkeleton.Vertex line 278
  35. def OAI.HardSphere.DyadicSkeleton.baseTrans line 280
  36. def OAI.HardSphere.DyadicSkeleton.baseVertex line 283
  37. lemma OAI.HardSphere.DyadicSkeleton.measurable_baseTrans line 286
  38. lemma OAI.HardSphere.DyadicSkeleton.measurable_baseVertex line 289
  39. lemma OAI.HardSphere.DyadicSkeleton.drift_rate_le line 298
  40. lemma OAI.HardSphere.DyadicSkeleton.baseTrans_lipschitz line 304
  41. lemma OAI.HardSphere.DyadicSkeleton.floor_abs_sub_le_two line 320
  42. lemma OAI.HardSphere.DyadicSkeleton.baseVertex_step line 338
  43. lemma OAI.HardSphere.DyadicSkeleton.baseVertex_initial line 350
  44. lemma OAI.HardSphere.DyadicSkeleton.baseVertex_final line 355
  45. def OAI.HardSphere.DyadicSkeleton.axisSteps line 361
  46. lemma OAI.HardSphere.DyadicSkeleton.axisSteps_length line 365
  47. lemma OAI.HardSphere.DyadicSkeleton.axisSteps_between line 376
  48. lemma OAI.HardSphere.DyadicSkeleton.axisSteps_near_final line 389
  49. def OAI.HardSphere.DyadicSkeleton.refineStep line 402
  50. lemma OAI.HardSphere.DyadicSkeleton.refineStep_length line 407