OAI/Probability/Ballisticity/Stationary/LocalEpisodeLog.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DirectionalTransience.episode_log_bound_local line 14
2. def OAI.DirectionalTransience.EpisodeChart.failsAt line 59
3. lemma OAI.DirectionalTransience.EpisodeChart.measurableSet_failsAt line 63
4. lemma OAI.DirectionalTransience.EpisodeChart.failsAt_eq line 73
5. def OAI.DirectionalTransience.EpisodeChart.countedNext line 77
6. def OAI.DirectionalTransience.EpisodeChart.countedBranch line 87
7. lemma OAI.DirectionalTransience.EpisodeChart.countedBranch_covers line 92
8. lemma OAI.DirectionalTransience.EpisodeChart.countedBranch_state line 103
9. lemma OAI.DirectionalTransience.EpisodeChart.countedBranch_record line 113
10. lemma OAI.DirectionalTransience.EpisodeChart.countedBranch_unique line 130