OAI/Analysis/HardSphere/Paths/LevelList.lean

GitHub source file

42 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.HardSphere.DyadicSkeleton.refineStep_mem line 12
  2. def OAI.HardSphere.DyadicSkeleton.levelList line 32
  3. def OAI.HardSphere.DyadicSkeleton.occurrenceList line 36
  4. lemma OAI.HardSphere.DyadicSkeleton.levelList_length line 39
  5. lemma OAI.HardSphere.DyadicSkeleton.levelList_mem line 46
  6. lemma OAI.HardSphere.DyadicSkeleton.occurrenceList_initial line 61
  7. lemma OAI.HardSphere.DyadicSkeleton.integer_step_lipschitz line 67
  8. lemma OAI.HardSphere.DyadicSkeleton.baseVertex_lipschitz line 87
  9. lemma OAI.HardSphere.DyadicSkeleton.real_sub_floor_le line 93
  10. lemma OAI.HardSphere.DyadicSkeleton.floor_sub_real_le line 103
  11. lemma OAI.HardSphere.DyadicSkeleton.same_time_position_bound line 113
  12. lemma OAI.HardSphere.DyadicSkeleton.same_time_floor_bound line 123
  13. def OAI.HardSphere.DyadicSkeleton.periodicProjection line 140
  14. def OAI.HardSphere.DyadicSkeleton.periodicDistance line 143
  15. lemma OAI.HardSphere.DyadicSkeleton.periodicDistance_nonneg line 146
  16. lemma OAI.HardSphere.DyadicSkeleton.periodicDistance_symm line 147
  17. lemma OAI.HardSphere.DyadicSkeleton.periodicDistance_triangle line 149
  18. lemma OAI.HardSphere.DyadicSkeleton.periodicDistance_le line 152
  19. lemma OAI.HardSphere.DyadicSkeleton.periodicDistance_coord line 160
  20. lemma OAI.HardSphere.DyadicSkeleton.periodicDistance_le_half line 172
  21. lemma OAI.HardSphere.DyadicSkeleton.same_time_deviation_le line 181
  22. lemma OAI.HardSphere.DyadicSkeleton.occurrence_deviation_le line 204
  23. def OAI.HardSphere.DyadicSkeleton.distanceToList line 252
  24. lemma OAI.HardSphere.DyadicSkeleton.distanceToList_nonneg line 255
  25. lemma OAI.HardSphere.DyadicSkeleton.distanceToList_le line 261
  26. lemma OAI.HardSphere.DyadicSkeleton.distanceToList_attained line 270
  27. lemma OAI.HardSphere.DyadicSkeleton.occurrenceList_ne_nil line 285
  28. lemma OAI.HardSphere.DyadicSkeleton.distanceToList_deviation_le line 288
  29. def OAI.HardSphere.DyadicSkeleton.foldIndex line 299
  30. lemma OAI.HardSphere.DyadicSkeleton.foldIndex_value line 303
  31. lemma OAI.HardSphere.DyadicSkeleton.foldIndex_injective line 310
  32. lemma OAI.HardSphere.DyadicSkeleton.folded_sum_le line 318
  33. lemma OAI.HardSphere.DyadicSkeleton.nearPotential_eq_if line 335
  34. lemma OAI.HardSphere.DyadicSkeleton.twoCopyDistance_swap line 343
  35. lemma OAI.HardSphere.DyadicSkeleton.nearPotential_swap line 348
  36. def OAI.HardSphere.DyadicSkeleton.oneSideHit line 355
  37. def OAI.HardSphere.DyadicSkeleton.occurrenceHit line 358
  38. def OAI.HardSphere.DyadicSkeleton.occurrenceSoft line 361
  39. lemma OAI.HardSphere.DyadicSkeleton.oneSideHit_nonneg line 364
  40. lemma OAI.HardSphere.DyadicSkeleton.occurrenceHit_nonneg line 371
  41. lemma OAI.HardSphere.DyadicSkeleton.level_sum_le line 375
  42. lemma OAI.HardSphere.DyadicSkeleton.oneSideHit_le line 402