OAI/Analysis/MarkovType/TwoLevels.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MarkovSuperreflexivity.wordMap_mem_openArc line 10
  2. theorem OAI.MarkovSuperreflexivity.wordMap_mem_arc line 20
  3. theorem OAI.MarkovSuperreflexivity.wordMap_mem_interior_arc line 24
  4. theorem OAI.MarkovSuperreflexivity.wordMap_zero_ne_int line 28
  5. theorem OAI.MarkovSuperreflexivity.wordCocycle_take_of_not_mem line 38
  6. theorem OAI.MarkovSuperreflexivity.wordCocycle_take_int line 61
  7. theorem OAI.MarkovSuperreflexivity.wordCocycle_take_upper_zero line 68
  8. theorem OAI.MarkovSuperreflexivity.wordCocycle_take_upper line 85
  9. theorem OAI.MarkovSuperreflexivity.wordCocycle_int_of_reduced line 92
  10. theorem OAI.MarkovSuperreflexivity.wordCocycle_upper_of_reduced line 96
  11. theorem OAI.MarkovSuperreflexivity.wordCocycle_int line 100
  12. theorem OAI.MarkovSuperreflexivity.wordCocycle_upper line 105
  13. theorem OAI.MarkovSuperreflexivity.wordCocycle_two_levels line 111
  14. theorem OAI.MarkovSuperreflexivity.wordCocycle_original_prefix_levels line 117
  15. theorem OAI.MarkovSuperreflexivity.wordCocycle_level_gap line 124
  16. theorem OAI.MarkovSuperreflexivity.wordMap_zero_ne_int_of_reduceWord_ne_nil line 129
  17. theorem OAI.MarkovSuperreflexivity.wordMap_zero_not_integer_iff line 134