OAI/Probability/Ballisticity/Estimates/VisitTrials.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DirectionalTransience.visitCount line 12
  2. lemma OAI.DirectionalTransience.visitCount_succ line 15
  3. lemma OAI.DirectionalTransience.visitCount_mono line 19
  4. lemma OAI.DirectionalTransience.visitCount_exists line 25
  5. lemma OAI.DirectionalTransience.measurable_visitCount line 38
  6. lemma OAI.DirectionalTransience.visitCount_prefix line 44
  7. def OAI.DirectionalTransience.VisitPrefix line 50
  8. def OAI.DirectionalTransience.VisitReached line 53
  9. lemma OAI.DirectionalTransience.measurableSet_visitPrefix line 56
  10. lemma OAI.DirectionalTransience.visitPrefix_prefix line 65
  11. lemma OAI.DirectionalTransience.measurableSet_visitReached line 76
  12. lemma OAI.DirectionalTransience.visitPrefix_disjoint line 79
  13. lemma OAI.DirectionalTransience.visitReached_succ_subset line 93
  14. def OAI.DirectionalTransience.ReturnIn line 100
  15. lemma OAI.DirectionalTransience.measurableSet_returnIn line 103
  16. lemma OAI.DirectionalTransience.visitReached_succ_return line 112
  17. lemma OAI.DirectionalTransience.visitReached_contraction line 126
  18. lemma OAI.DirectionalTransience.visitReached_geometric line 152