OAI/Probability/Ballisticity/Stationary/ArrayMap.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.DirectionalTransience.enat_borel line 12
  2. instance OAI.DirectionalTransience.horizontalOnePoint_measurable line 13
  3. instance OAI.DirectionalTransience.horizontalOnePoint_borel line 15
  4. def OAI.DirectionalTransience.episodeProfile line 18
  5. instance OAI.DirectionalTransience.episodeProfile_probability line 22
  6. lemma OAI.DirectionalTransience.globalHorizontalProfile_joint_measurable line 28
  7. lemma OAI.DirectionalTransience.globalHorizontalCoordinate_joint_measurable line 34
  8. abbrev OAI.DirectionalTransience.EpisodeAnchors line 43
  9. abbrev OAI.DirectionalTransience.EpisodeAuxiliary line 44
  10. abbrev OAI.DirectionalTransience.EpisodeInput line 45
  11. lemma OAI.DirectionalTransience.episodeProfile_measurable line 47
  12. def OAI.DirectionalTransience.globalEpisodeAnchors line 54
  13. instance OAI.DirectionalTransience.globalEpisodeAnchors_markov line 60
  14. def OAI.DirectionalTransience.episodeAuxiliaryLaw line 64
  15. instance OAI.DirectionalTransience.episodeAuxiliaryLaw_probability line 68
  16. def OAI.DirectionalTransience.episodeInputLaw line 72
  17. instance OAI.DirectionalTransience.episodeInputLaw_probability line 77
  18. def OAI.DirectionalTransience.episodeCost line 82
  19. lemma OAI.DirectionalTransience.episodeCost_measurable line 87
  20. def OAI.DirectionalTransience.episodeSplicedRow line 97
  21. def OAI.DirectionalTransience.actualArrayMap line 104
  22. lemma OAI.DirectionalTransience.episodeSplicedRow_measurable line 111
  23. lemma OAI.DirectionalTransience.actualArrayCoordinate_measurable line 129
  24. lemma OAI.DirectionalTransience.actualArrayMap_measurable line 141