OAI/Probability/DirectionalWalk/ContactGeometry.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DirectionalZeroOne.oppositeStep line 12
  2. lemma OAI.DirectionalZeroOne.axisDirection_opposite line 14
  3. lemma OAI.DirectionalZeroOne.axisHeight_opposite line 20
  4. lemma OAI.DirectionalZeroOne.axisHeight_neg line 25
  5. lemma OAI.DirectionalZeroOne.axisHeight_sum line 30
  6. lemma OAI.DirectionalZeroOne.axisHeight_step_self line 37
  7. lemma OAI.DirectionalZeroOne.axisHeight_wordEnd line 41
  8. lemma OAI.DirectionalZeroOne.axisHeight_word_interior line 49
  9. def OAI.DirectionalZeroOne.placedAxis line 59
  10. def OAI.DirectionalZeroOne.placedWidth line 61
  11. def OAI.DirectionalZeroOne.opposedAnchor line 64
  12. def OAI.DirectionalZeroOne.opposedSite line 68
  13. def OAI.DirectionalZeroOne.opposedDeparture line 71
  14. def OAI.DirectionalZeroOne.contactAt line 74
  15. def OAI.DirectionalZeroOne.contactDepth line 77
  16. lemma OAI.DirectionalZeroOne.opposedAnchor_height line 80
  17. lemma OAI.DirectionalZeroOne.opposed_departure_band line 95
  18. lemma OAI.DirectionalZeroOne.axial_step_unique line 117
  19. lemma OAI.DirectionalZeroOne.axis_word_last_step line 126
  20. lemma OAI.DirectionalZeroOne.opposed_forced_contact line 142
  21. def OAI.DirectionalZeroOne.axisLower line 159
  22. def OAI.DirectionalZeroOne.axisUpper line 160
  23. lemma OAI.DirectionalZeroOne.axis_barriers_disjoint line 162
  24. lemma OAI.DirectionalZeroOne.hitBefore_axis_eq_reach line 168
  25. lemma OAI.DirectionalZeroOne.annealed_axis_exit line 179
  26. lemma OAI.DirectionalZeroOne.annealed_axis_return_probability line 195
  27. lemma OAI.DirectionalZeroOne.annealed_axis_visitAfter_bound line 225