OAI/Analysis/MarkovType/IntegerCocycle.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MarkovSuperreflexivity.arcIndicator line 14
  2. def OAI.MarkovSuperreflexivity.negativeIndicator line 18
  3. def OAI.MarkovSuperreflexivity.chi line 20
  4. theorem OAI.MarkovSuperreflexivity.chi_of_mem line 22
  5. theorem OAI.MarkovSuperreflexivity.chi_of_not_mem line 26
  6. theorem OAI.MarkovSuperreflexivity.negativeIndicator_inv line 30
  7. theorem OAI.MarkovSuperreflexivity.arcIndicator_inv_symm line 35
  8. theorem OAI.MarkovSuperreflexivity.chi_inv_symm line 46
  9. theorem OAI.MarkovSuperreflexivity.chi_add_int line 51
  10. def OAI.MarkovSuperreflexivity.wordCocycle line 61
  11. theorem OAI.MarkovSuperreflexivity.wordCocycle_nil line 65
  12. theorem OAI.MarkovSuperreflexivity.wordCocycle_cons line 67
  13. theorem OAI.MarkovSuperreflexivity.wordCocycle_append line 71
  14. theorem OAI.MarkovSuperreflexivity.wordCocycle_cancel line 80
  15. theorem OAI.MarkovSuperreflexivity.wordCocycle_reduceWord line 89
  16. theorem OAI.MarkovSuperreflexivity.letter_symm_add_int line 94
  17. theorem OAI.MarkovSuperreflexivity.wordCocycle_add_int line 100
  18. theorem OAI.MarkovSuperreflexivity.wordCocycle_inverseWord line 107
  19. def OAI.MarkovSuperreflexivity.pullbackPoint line 117
  20. theorem OAI.MarkovSuperreflexivity.pullbackPoint_zero line 120
  21. theorem OAI.MarkovSuperreflexivity.pullbackPoint_nil line 123
  22. theorem OAI.MarkovSuperreflexivity.pullbackPoint_cons_succ line 127
  23. theorem OAI.MarkovSuperreflexivity.pullbackPoint_succ line 132
  24. theorem OAI.MarkovSuperreflexivity.letterOrderIso_pullbackPoint_succ line 146
  25. theorem OAI.MarkovSuperreflexivity.pullbackPoint_wordMap line 152
  26. theorem OAI.MarkovSuperreflexivity.pullbackPoint_add_int line 156
  27. theorem OAI.MarkovSuperreflexivity.pullbackPoint_int line 160
  28. theorem OAI.MarkovSuperreflexivity.pullbackPoint_wordMap_add_int line 165
  29. theorem OAI.MarkovSuperreflexivity.wordCocycle_eq_sum line 170