OAI/Analysis/MarkovType/WalkParameters.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MarkovSuperreflexivity.walkWindowLength line 13
  2. def OAI.MarkovSuperreflexivity.walkWindowLeft line 15
  3. def OAI.MarkovSuperreflexivity.walkWindowRight line 17
  4. def OAI.MarkovSuperreflexivity.walkWindowPairs line 19
  5. def OAI.MarkovSuperreflexivity.walkError line 21
  6. theorem OAI.MarkovSuperreflexivity.walkWindowLength_pos line 23
  7. theorem OAI.MarkovSuperreflexivity.walkWindowPairs_pos line 26
  8. theorem OAI.MarkovSuperreflexivity.walkWindowLength_eq_twice_pairs line 29
  9. theorem OAI.MarkovSuperreflexivity.walkWindowRight_sub_left line 34
  10. theorem OAI.MarkovSuperreflexivity.walkWindowLeft_lt_right line 39
  11. theorem OAI.MarkovSuperreflexivity.walkWindowRight_lt_length line 43
  12. theorem OAI.MarkovSuperreflexivity.walkError_pos line 47
  13. theorem OAI.MarkovSuperreflexivity.mul_walkError line 51
  14. theorem OAI.MarkovSuperreflexivity.walk_floor_bounds line 57
  15. theorem OAI.MarkovSuperreflexivity.walk_fractional_bounds line 71
  16. theorem OAI.MarkovSuperreflexivity.walk_shift_bounds line 80
  17. theorem OAI.MarkovSuperreflexivity.walk_integer_shift_mem_range line 89
  18. theorem OAI.MarkovSuperreflexivity.walk_translated_shift_mem_range line 97
  19. theorem OAI.MarkovSuperreflexivity.walk_transport_in_window line 107