OAI/Probability/Ballisticity/Stationary/EpisodeCharts.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.DirectionalTransience.EpisodeState.ext_raw line 12
  2. structure OAI.DirectionalTransience.EpisodeChart line 24
  3. def OAI.DirectionalTransience.EpisodeChart.state line 35
  4. def OAI.DirectionalTransience.EpisodeChart.layerProfile line 38
  5. lemma OAI.DirectionalTransience.EpisodeChart.measurable_layerProfile line 41
  6. def OAI.DirectionalTransience.EpisodeChart.stop line 45
  7. def OAI.DirectionalTransience.EpisodeChart.growsAt line 49
  8. lemma OAI.DirectionalTransience.EpisodeChart.measurableSet_growsAt line 54
  9. lemma OAI.DirectionalTransience.EpisodeChart.stop_eq line 64
  10. lemma OAI.DirectionalTransience.EpisodeChart.growsAt_eq line 67
  11. def OAI.DirectionalTransience.EpisodeChart.nextScale line 73
  12. def OAI.DirectionalTransience.EpisodeChart.nextProfile line 76
  13. lemma OAI.DirectionalTransience.EpisodeChart.measurable_nextProfile line 83
  14. def OAI.DirectionalTransience.EpisodeChart.nextEvent line 93
  15. lemma OAI.DirectionalTransience.EpisodeChart.measurable_nextEvent line 98
  16. def OAI.DirectionalTransience.EpisodeChart.next line 125
  17. lemma OAI.DirectionalTransience.episodeStageNext_profile line 145
  18. lemma OAI.DirectionalTransience.EpisodeChart.next_state line 160
  19. def OAI.DirectionalTransience.EpisodeChart.frozen line 190
  20. def OAI.DirectionalTransience.EpisodeChart.branch line 198
  21. lemma OAI.DirectionalTransience.EpisodeChart.branch_covers line 203
  22. lemma OAI.DirectionalTransience.EpisodeChart.branch_state line 213
  23. structure OAI.DirectionalTransience.EpisodeAtlas line 230
  24. def OAI.DirectionalTransience.EpisodeAtlas.advance line 242
  25. def OAI.DirectionalTransience.EpisodeAtlas.run line 258
  26. lemma OAI.DirectionalTransience.EpisodeAtlas.height_event line 265
  27. lemma OAI.DirectionalTransience.EpisodeAtlas.profile_event line 286