OAI/Analysis/MarkovType/PeriodicOrderIso.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MarkovSuperreflexivity.periodicLiftFun line 16
  2. theorem OAI.MarkovSuperreflexivity.periodicLiftFun_range line 19
  3. theorem OAI.MarkovSuperreflexivity.periodicLiftFun_floor line 25
  4. theorem OAI.MarkovSuperreflexivity.periodicLiftFun_fract line 32
  5. theorem OAI.MarkovSuperreflexivity.periodicLiftFun_strictMono line 38
  6. theorem OAI.MarkovSuperreflexivity.periodicLiftFun_rightInverse line 58
  7. def OAI.MarkovSuperreflexivity.unitPeriodicOrderIso line 76
  8. theorem OAI.MarkovSuperreflexivity.unitPeriodicOrderIso_apply line 81
  9. theorem OAI.MarkovSuperreflexivity.unitPeriodicOrderIso_symm_apply line 84
  10. theorem OAI.MarkovSuperreflexivity.periodicLiftFun_add_int line 88
  11. theorem OAI.MarkovSuperreflexivity.periodicLiftFun_int line 93
  12. theorem OAI.MarkovSuperreflexivity.periodicLiftFun_of_mem_Ico line 97
  13. def OAI.MarkovSuperreflexivity.twoSlope line 102
  14. def OAI.MarkovSuperreflexivity.twoSlopeInverse line 104
  15. theorem OAI.MarkovSuperreflexivity.twoSlope_strictMono line 106
  16. theorem OAI.MarkovSuperreflexivity.twoSlope_rightInverse line 111
  17. def OAI.MarkovSuperreflexivity.twoSlopeOrderIso line 121
  18. theorem OAI.MarkovSuperreflexivity.twoSlopeOrderIso_apply line 125
  19. theorem OAI.MarkovSuperreflexivity.twoSlopeOrderIso_symm_apply line 127
  20. theorem OAI.MarkovSuperreflexivity.twoSlopeOrderIso_zero line 130
  21. theorem OAI.MarkovSuperreflexivity.twoSlopeOrderIso_one line 133
  22. def OAI.MarkovSuperreflexivity.periodicBend line 136
  23. theorem OAI.MarkovSuperreflexivity.periodicBend_apply line 139
  24. theorem OAI.MarkovSuperreflexivity.periodicBend_symm_apply line 142
  25. theorem OAI.MarkovSuperreflexivity.periodicBend_add_int line 145
  26. theorem OAI.MarkovSuperreflexivity.periodicBend_symm_add_int line 149
  27. theorem OAI.MarkovSuperreflexivity.periodicBend_int line 153
  28. theorem OAI.MarkovSuperreflexivity.periodicBend_zero line 156
  29. theorem OAI.MarkovSuperreflexivity.periodicBend_one line 159
  30. theorem OAI.MarkovSuperreflexivity.periodicBend_eq_twoSlope line 162
  31. theorem OAI.MarkovSuperreflexivity.periodicBend_ninth line 169
  32. theorem OAI.MarkovSuperreflexivity.periodicBend_displacement line 173
  33. def OAI.MarkovSuperreflexivity.translatedPeriodicOrderIso line 185
  34. theorem OAI.MarkovSuperreflexivity.translatedPeriodicOrderIso_apply line 195
  35. theorem OAI.MarkovSuperreflexivity.translatedPeriodicOrderIso_symm_apply line 198
  36. theorem OAI.MarkovSuperreflexivity.translatedPeriodicOrderIso_add_int line 201
  37. theorem OAI.MarkovSuperreflexivity.translatedPeriodicOrderIso_symm_add_int line 207
  38. theorem OAI.MarkovSuperreflexivity.translatedPeriodicOrderIso_start line 214
  39. theorem OAI.MarkovSuperreflexivity.translatedPeriodicOrderIso_break line 218
  40. theorem OAI.MarkovSuperreflexivity.translatedPeriodicOrderIso_end line 222
  41. theorem OAI.MarkovSuperreflexivity.translatedPeriodicOrderIso_displacement line 226
  42. theorem OAI.MarkovSuperreflexivity.translatedPeriodicOrderIso_left line 233
  43. theorem OAI.MarkovSuperreflexivity.translatedPeriodicOrderIso_right line 240
  44. theorem OAI.MarkovSuperreflexivity.translatedPeriodicOrderIso_inverse_left line 248
  45. theorem OAI.MarkovSuperreflexivity.translatedPeriodicOrderIso_inverse_right line 256