OAI/Analysis/MarkovType/MarkedPaths.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MarkovSuperreflexivity.markedTransition line 16
  2. theorem OAI.MarkovSuperreflexivity.markedTransition_nonneg line 20
  3. theorem OAI.MarkovSuperreflexivity.sum_markedTransition line 28
  4. theorem OAI.MarkovSuperreflexivity.markedTransition_balance line 40
  5. def OAI.MarkovSuperreflexivity.FiniteMarkedChain.toStateChain line 56
  6. theorem OAI.MarkovSuperreflexivity.markedState_zero line 66
  7. theorem OAI.MarkovSuperreflexivity.markedState_succ line 70
  8. def OAI.MarkovSuperreflexivity.markedSnoc line 75
  9. theorem OAI.MarkovSuperreflexivity.markedState_snoc_castSucc line 78
  10. theorem OAI.MarkovSuperreflexivity.markedState_snoc line 86
  11. theorem OAI.MarkovSuperreflexivity.markedValid_snoc line 96
  12. theorem OAI.MarkovSuperreflexivity.markedPathWeight_nonneg line 117
  13. theorem OAI.MarkovSuperreflexivity.markedPathWeight_eq_zero_of_not_valid line 125
  14. theorem OAI.MarkovSuperreflexivity.markedPathWeight_of_valid line 129
  15. theorem OAI.MarkovSuperreflexivity.markedPathWeight_snoc line 134
  16. theorem OAI.MarkovSuperreflexivity.markedExpect_snoc line 149
  17. theorem OAI.MarkovSuperreflexivity.sum_markedPathWeight line 169
  18. def OAI.MarkovSuperreflexivity.markedLaw line 182
  19. theorem OAI.MarkovSuperreflexivity.sum_outgoing_target line 187
  20. theorem OAI.MarkovSuperreflexivity.markedExpect_state line 198
  21. def OAI.MarkovSuperreflexivity.markedTake line 244
  22. theorem OAI.MarkovSuperreflexivity.markedTake_self line 249
  23. theorem OAI.MarkovSuperreflexivity.markedTake_snoc line 256
  24. theorem OAI.MarkovSuperreflexivity.markedExpect_take line 266
  25. theorem OAI.MarkovSuperreflexivity.markedExpect_last_edge line 286
  26. theorem OAI.MarkovSuperreflexivity.markedExpect_edge line 306