OAI/Probability/Ballisticity/Stationary/EpisodeAdapted.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DirectionalTransience.episodeInitialChart line 13
  2. def OAI.DirectionalTransience.episodeInitialAtlas line 30
  3. def OAI.DirectionalTransience.episodeFinalAtlas line 39
  4. lemma OAI.DirectionalTransience.episodeFinal_height_event line 44
  5. lemma OAI.DirectionalTransience.episodeBoundary_height_event line 50
  6. lemma OAI.DirectionalTransience.EpisodeChart.branch_unique line 107
  7. def OAI.DirectionalTransience.EpisodeAtlas.IsPartition line 134
  8. lemma OAI.DirectionalTransience.EpisodeAtlas.advance_partition line 137
  9. lemma OAI.DirectionalTransience.EpisodeAtlas.run_partition line 147
  10. lemma OAI.DirectionalTransience.EpisodeAtlas.chart_disjoint line 154
  11. lemma OAI.DirectionalTransience.episodeInitialAtlas_partition line 161
  12. lemma OAI.DirectionalTransience.episodeFinalAtlas_partition line 169