OAI/Probability/Ballisticity/Stationary/EpisodeRetention.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DirectionalTransience.episodeStageNext_retained line 12
2. def OAI.DirectionalTransience.episodeSteps line 47
3. lemma OAI.DirectionalTransience.episodeRun_height_mono line 54
4. def OAI.DirectionalTransience.episodeMeasure line 67
5. theorem OAI.DirectionalTransience.episodeRun_retained line 70
6. def OAI.DirectionalTransience.StageRadiusOrder line 125
7. lemma OAI.DirectionalTransience.episodeStageNext_retained_local line 128
8. theorem OAI.DirectionalTransience.episodeRun_retained_local line 160