OAI/Probability/Ballisticity/Crossings/FiniteBoxExit.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.DirectionalTransience.sum_visitCount line 13
  2. lemma OAI.DirectionalTransience.visitCount_pigeonhole line 26
  3. def OAI.DirectionalTransience.ConfinedUntil line 36
  4. lemma OAI.DirectionalTransience.measurableSet_confinedUntil line 39
  5. lemma OAI.DirectionalTransience.confinedUntil_subset_visits line 47
  6. lemma OAI.DirectionalTransience.visitReached_empty line 56
  7. lemma OAI.DirectionalTransience.quenched_confinedUntil_bound line 65
  8. def OAI.DirectionalTransience.UpwardCross line 94
  9. lemma OAI.DirectionalTransience.measurableSet_upwardCross line 98
  10. lemma OAI.DirectionalTransience.quenched_upwardCross line 102
  11. lemma OAI.DirectionalTransience.upwardCross_no_return line 110
  12. lemma OAI.DirectionalTransience.upwardCross_success line 136
  13. lemma OAI.DirectionalTransience.quenched_stripBox_exit_bound line 144