OAI/Analysis/MarkovType/FinitePaths.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MarkovSuperreflexivity.sum_π_mul_P line 20
  2. theorem OAI.MarkovSuperreflexivity.balance_product line 25
  3. def OAI.MarkovSuperreflexivity.pathReverse line 46
  4. theorem OAI.MarkovSuperreflexivity.pathReverse_reverse line 50
  5. def OAI.MarkovSuperreflexivity.pathReverseEquiv line 55
  6. theorem OAI.MarkovSuperreflexivity.pathWeight_reverse line 61
  7. theorem OAI.MarkovSuperreflexivity.pathWeight_snoc line 74
  8. theorem OAI.MarkovSuperreflexivity.sum_pathWeight_snoc_v line 88
  9. theorem OAI.MarkovSuperreflexivity.sum_pathWeight_reverse_v line 101
  10. theorem OAI.MarkovSuperreflexivity.sum_pathWeight_snoc line 112
  11. theorem OAI.MarkovSuperreflexivity.sum_pathWeight line 119
  12. def OAI.MarkovSuperreflexivity.pathLaw line 138
  13. def OAI.MarkovSuperreflexivity.pathTake line 143
  14. def OAI.MarkovSuperreflexivity.pathPrefix line 146
  15. theorem OAI.MarkovSuperreflexivity.pathTake_self line 150
  16. theorem OAI.MarkovSuperreflexivity.pathTake_snoc line 156
  17. theorem OAI.MarkovSuperreflexivity.sum_pathWeight_take_v line 170
  18. theorem OAI.MarkovSuperreflexivity.sum_pathWeight_take line 193
  19. theorem OAI.MarkovSuperreflexivity.sum_pathWeight_prefix line 199
  20. theorem OAI.MarkovSuperreflexivity.sum_pathWeight_last line 205
  21. theorem OAI.MarkovSuperreflexivity.sum_pathWeight_last_pair line 227
  22. theorem OAI.MarkovSuperreflexivity.sum_pathWeight_pair line 238
  23. theorem OAI.MarkovSuperreflexivity.stateCost_one line 255
  24. theorem OAI.MarkovSuperreflexivity.sum_pathWeight_take_next line 262