OAI/Probability/Ballisticity/Estimates/GridTrials.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DirectionalTransience.DropBetween line 12
  2. lemma OAI.DirectionalTransience.measurableSet_dropBetween line 15
  3. lemma OAI.DirectionalTransience.dropBetween_prefix line 23
  4. lemma OAI.DirectionalTransience.dropBetween_not_futureNoDrop line 30
  5. def OAI.DirectionalTransience.GridPrefix line 38
  6. def OAI.DirectionalTransience.GridReached line 43
  7. lemma OAI.DirectionalTransience.gridPrefix_hit line 46
  8. lemma OAI.DirectionalTransience.measurableSet_gridPrefix line 52
  9. lemma OAI.DirectionalTransience.measurableSet_gridReached line 63
  10. lemma OAI.DirectionalTransience.gridPrefix_prefix line 66
  11. lemma OAI.DirectionalTransience.gridPrefix_disjoint line 84
  12. lemma OAI.DirectionalTransience.gridPrefix_record line 91
  13. lemma OAI.DirectionalTransience.gridReached_succ_subset line 103
  14. lemma OAI.DirectionalTransience.gridReached_succ_failure line 111
  15. lemma OAI.DirectionalTransience.gridReached_contraction line 123
  16. lemma OAI.DirectionalTransience.gridReached_geometric line 154