OAI/Probability/Ballisticity/Stationary/EpisodeCountLedger.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DirectionalTransience.episodeStageIncomplete line 13
  2. lemma OAI.DirectionalTransience.EpisodeLedger.counts_partition line 29
  3. lemma OAI.DirectionalTransience.EpisodeLedger.incomplete_count line 50
  4. lemma OAI.DirectionalTransience.EpisodeLedger.counts_le line 68
  5. lemma OAI.DirectionalTransience.EpisodeLedger.nonterminal_ledger line 79
  6. lemma OAI.DirectionalTransience.EpisodeLedger.terminal_ledger line 93
  7. def OAI.DirectionalTransience.EpisodeChainLedger.count line 128
  8. def OAI.DirectionalTransience.EpisodeChainLedger.steps line 132
  9. lemma OAI.DirectionalTransience.EpisodeChainLedger.partition line 139
  10. lemma OAI.DirectionalTransience.EpisodeChainLedger.incomplete line 150
  11. lemma OAI.DirectionalTransience.EpisodeChainLedger.counts_le line 162
  12. lemma OAI.DirectionalTransience.EpisodeChainLedger.balance line 167
  13. theorem OAI.DirectionalTransience.EpisodeChainLedger.stage_count_bound line 196