OAI/Probability/Ballisticity/Stationary/EpisodeMeanDrop.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.DirectionalTransience.EpisodeChainLedger.mean_episode_drops line 19
2. lemma OAI.DirectionalTransience.EpisodeChainLedger.dropMark_bounds_local line 118
3. lemma OAI.DirectionalTransience.EpisodeChainLedger.total_drop_bound_local line 131
4. lemma OAI.DirectionalTransience.EpisodeChainLedger.long_drop_bound_local line 148
5. lemma OAI.DirectionalTransience.EpisodeChainLedger.dropMark_integrable_local line 180
6. theorem OAI.DirectionalTransience.EpisodeChainLedger.mean_episode_drops_local line 197