OAI/Probability/Ballisticity/Stationary/OperationalEpisode.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.DirectionalTransience.EpisodeState line 12
  2. def OAI.DirectionalTransience.episodeStageH line 17
  3. def OAI.DirectionalTransience.episodeStageLength line 19
  4. def OAI.DirectionalTransience.EpisodeReady line 25
  5. def OAI.DirectionalTransience.episodeStageGrows line 29
  6. def OAI.DirectionalTransience.episodeStageScale line 37
  7. lemma OAI.DirectionalTransience.episodeStageGap line 42
  8. def OAI.DirectionalTransience.episodeStageNext line 53
  9. lemma OAI.DirectionalTransience.episodeStageNext_height line 67
  10. lemma OAI.DirectionalTransience.episodeStageNext_le line 73
  11. lemma OAI.DirectionalTransience.episodeStageNext_gt line 84
  12. def OAI.DirectionalTransience.episodeRun line 94
  13. lemma OAI.DirectionalTransience.episodeRun_le line 101
  14. lemma OAI.DirectionalTransience.episodeRun_progress line 113
  15. theorem OAI.DirectionalTransience.episodeRun_terminates line 131