OAI/Probability/Ballisticity/Stationary/EpisodeDropLedger.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DirectionalTransience.EpisodeChainLedger.stepMark line 19
  2. def OAI.DirectionalTransience.EpisodeChainLedger.dropMark line 23
  3. lemma OAI.DirectionalTransience.EpisodeChainLedger.stepMark_sub line 29
  4. lemma OAI.DirectionalTransience.EpisodeChainLedger.stepMark_measurable line 33
  5. lemma OAI.DirectionalTransience.EpisodeChainLedger.dropMark_measurable line 40
  6. lemma OAI.DirectionalTransience.EpisodeChainLedger.stepMark_sum line 48
  7. lemma OAI.DirectionalTransience.EpisodeChainLedger.dropMark_sum line 53
  8. lemma OAI.DirectionalTransience.EpisodeChainLedger.dropMark_total line 60
  9. lemma OAI.DirectionalTransience.EpisodeChainLedger.dropMark_bounds line 64
  10. lemma OAI.DirectionalTransience.EpisodeChainLedger.total_drop_bound line 77
  11. lemma OAI.DirectionalTransience.EpisodeChainLedger.stepMark_le line 111
  12. lemma OAI.DirectionalTransience.EpisodeChainLedger.dropMark_inactive line 118
  13. lemma OAI.DirectionalTransience.EpisodeChainLedger.injection_cost_nonneg line 124
  14. lemma OAI.DirectionalTransience.EpisodeChainLedger.long_drop_bound line 129
  15. lemma OAI.DirectionalTransience.EpisodeChainLedger.dropMark_integrable line 161