OAI/Probability/Ballisticity/Stationary/BadCrossingEpisodes.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.DirectionalTransience.OperationalConstants.radius_nonneg line 18
  2. def OAI.DirectionalTransience.OperationalConstants.activeCount line 22
  3. def OAI.DirectionalTransience.OperationalConstants.stagesAt line 27
  4. def OAI.DirectionalTransience.OperationalConstants.dropAt line 32
  5. def OAI.DirectionalTransience.OperationalConstants.injectionCost line 37
  6. lemma OAI.DirectionalTransience.OperationalConstants.height_pos line 40
  7. lemma OAI.DirectionalTransience.OperationalConstants.cost_nonneg line 46
  8. lemma OAI.DirectionalTransience.OperationalConstants.finite_charge line 49
  9. theorem OAI.DirectionalTransience.OperationalConstants.conditional_episode_drops line 59
  10. lemma OAI.DirectionalTransience.episodeInputLaw_environment line 113
  11. lemma OAI.DirectionalTransience.episodeInputLaw_env_integral line 123
  12. def OAI.DirectionalTransience.EpisodeChainLedger.arrayTime line 141
  13. def OAI.DirectionalTransience.EpisodeChainLedger.arrayStages line 142
  14. lemma OAI.DirectionalTransience.EpisodeChainLedger.arrayTime_measurable line 147
  15. lemma OAI.DirectionalTransience.EpisodeChainLedger.arrayStages_measurable line 149
  16. lemma OAI.DirectionalTransience.EpisodeChainLedger.arrayTime_neg line 155
  17. lemma OAI.DirectionalTransience.EpisodeChainLedger.arrayTime_nat line 158
  18. lemma OAI.DirectionalTransience.EpisodeChainLedger.arrayTime_terminal line 161
  19. lemma OAI.DirectionalTransience.EpisodeChainLedger.arrayStages_nat line 168
  20. lemma OAI.DirectionalTransience.EpisodeChainLedger.arrayStages_terminal line 171
  21. lemma OAI.DirectionalTransience.EpisodeChainLedger.operational_raw_mass line 178
  22. lemma OAI.DirectionalTransience.EpisodeChainLedger.operational_mass_positive line 193