OAI/Analysis/HardSphere/Paths/LiftedSkeleton.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HardSphere.DyadicSkeleton.mem_axisSteps_of_between line 16
  2. lemma OAI.HardSphere.DyadicSkeleton.refineStep_final line 32
  3. lemma OAI.HardSphere.DyadicSkeleton.refineStep_reach line 48
  4. lemma OAI.HardSphere.DyadicSkeleton.baseVertex_mem_level line 89
  5. lemma OAI.HardSphere.DyadicSkeleton.level_mem_occurrence line 95
  6. lemma OAI.HardSphere.DyadicSkeleton.occurrence_reach line 99
  7. lemma OAI.HardSphere.DyadicSkeleton.nearestStep_add line 120
  8. lemma OAI.HardSphere.DyadicSkeleton.withinReach_add line 126
  9. def OAI.HardSphere.DyadicSkeleton.liftedSkeleton line 134
  10. lemma OAI.HardSphere.DyadicSkeleton.liftedSkeleton_mem line 137
  11. lemma OAI.HardSphere.DyadicSkeleton.liftedSkeleton_reach line 141
  12. lemma OAI.HardSphere.DyadicSkeleton.liftedSkeleton_initial line 148
  13. lemma OAI.HardSphere.DyadicSkeleton.liftedSkeleton_final line 152
  14. instance OAI.HardSphere.DyadicSkeleton.finsetVertexMeasurableSpace line 159
  15. instance OAI.HardSphere.DyadicSkeleton.finsetVertexDiscreteMeasurableSpace line 160
  16. lemma OAI.HardSphere.DyadicSkeleton.measurable_liftedSkeleton line 163
  17. def OAI.HardSphere.DyadicSkeleton.ConnectedSkeleton line 168
  18. instance OAI.HardSphere.DyadicSkeleton.(instance at line 171) line 171
  19. instance OAI.HardSphere.DyadicSkeleton.(instance at line 173) line 173
  20. instance OAI.HardSphere.DyadicSkeleton.(instance at line 175) line 175
  21. lemma OAI.HardSphere.DyadicSkeleton.exists_connected_detour line 178
  22. def OAI.HardSphere.DyadicSkeleton.connectedDetour line 189
  23. lemma OAI.HardSphere.DyadicSkeleton.connectedDetour_spec line 195
  24. def OAI.HardSphere.DyadicSkeleton.connectedSample line 204
  25. lemma OAI.HardSphere.DyadicSkeleton.measurable_connectedSample line 210
  26. def OAI.HardSphere.DyadicSkeleton.dyadicDetour line 214
  27. lemma OAI.HardSphere.DyadicSkeleton.measurable_dyadicDetour line 220
  28. lemma OAI.HardSphere.DyadicSkeleton.dyadicDetour_spec line 227
  29. def OAI.HardSphere.DyadicSkeleton.nominalBase line 235
  30. def OAI.HardSphere.DyadicSkeleton.projectedSkeleton line 238
  31. lemma OAI.HardSphere.DyadicSkeleton.nominalBase_first line 241
  32. lemma OAI.HardSphere.DyadicSkeleton.nominalBase_speed line 244
  33. lemma OAI.HardSphere.DyadicSkeleton.projectedSkeleton_cover line 252
  34. lemma OAI.HardSphere.DyadicSkeleton.nominalBase_near_deviation line 266
  35. lemma OAI.HardSphere.DyadicSkeleton.dyadicDetour_charge line 287
  36. lemma OAI.HardSphere.DyadicSkeleton.geometric_term_soft line 309
  37. lemma OAI.HardSphere.DyadicSkeleton.geometric_soft_sum line 329
  38. lemma OAI.HardSphere.DyadicSkeleton.exp_soft_dominates_one line 348
  39. def OAI.HardSphere.DyadicSkeleton.dyadicRadius line 355
  40. lemma OAI.HardSphere.DyadicSkeleton.dyadicRadius_pos line 357
  41. lemma OAI.HardSphere.DyadicSkeleton.dyadic_nominal_potential line 359