OAI/Analysis/MarkovType/WalkLandmarks.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MarkovSuperreflexivity.WalkBoundedWord line 13
  2. def OAI.MarkovSuperreflexivity.WalkBoundedWord.toList line 15
  3. theorem OAI.MarkovSuperreflexivity.WalkBoundedWord.length_toList line 18
  4. theorem OAI.MarkovSuperreflexivity.WalkBoundedWord.length_toList_le line 22
  5. def OAI.MarkovSuperreflexivity.WalkBoundedWord.ofList line 27
  6. theorem OAI.MarkovSuperreflexivity.WalkBoundedWord.toList_ofList line 31
  7. def OAI.MarkovSuperreflexivity.walkLandmarkShifts line 35
  8. def OAI.MarkovSuperreflexivity.walkEndpointValue line 38
  9. def OAI.MarkovSuperreflexivity.walkEndpoints line 43
  10. def OAI.MarkovSuperreflexivity.walkOrbitPoints line 47
  11. def OAI.MarkovSuperreflexivity.walkLandmarks line 52
  12. theorem OAI.MarkovSuperreflexivity.alpha_shift_mem_walkLandmarks line 56
  13. theorem OAI.MarkovSuperreflexivity.beta_shift_mem_walkLandmarks line 66
  14. theorem OAI.MarkovSuperreflexivity.orbit_shift_mem_walkLandmarks line 76
  15. theorem OAI.MarkovSuperreflexivity.integer_mem_walkLandmarks line 90
  16. theorem OAI.MarkovSuperreflexivity.zero_mem_walkLandmarks line 98
  17. theorem OAI.MarkovSuperreflexivity.length_mem_walkLandmarks line 104
  18. theorem OAI.MarkovSuperreflexivity.walkLandmarks_nonempty line 111
  19. theorem OAI.MarkovSuperreflexivity.sampled_integer_mem_walkLandmarks line 114
  20. theorem OAI.MarkovSuperreflexivity.translated_orbit_mem_walkLandmarks line 121