OAI/Probability/DirectionalWalk/Regeneration.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DirectionalZeroOne.strictRecord line 10
  2. def OAI.DirectionalZeroOne.trueCut line 13
  3. lemma OAI.DirectionalZeroOne.measurableSet_strictRecord line 16
  4. lemma OAI.DirectionalZeroOne.measurableSet_trueCut line 24
  5. lemma OAI.DirectionalZeroOne.strictRecord_prefix line 31
  6. lemma OAI.DirectionalZeroOne.unbounded_has_later_strictRecord line 37
  7. lemma OAI.DirectionalZeroOne.measurableSet_boundedHeight line 59
  8. lemma OAI.DirectionalZeroOne.no_later_trueCut_null line 72
  9. lemma OAI.DirectionalZeroOne.ae_infinitely_trueCuts line 106
  10. lemma OAI.DirectionalZeroOne.escape_of_infinitely_trueCuts line 119
  11. lemma OAI.DirectionalZeroOne.height_neg_direction line 134
  12. lemma OAI.DirectionalZeroOne.ae_escape_or_opposite line 137
  13. def OAI.DirectionalZeroOne.nearestNeighbour line 149
  14. lemma OAI.DirectionalZeroOne.ae_start_and_nearestNeighbour line 152