OAI/Analysis/MarkovType/WalkTransport.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MarkovSuperreflexivity.walkOrbitFloor line 13
  2. def OAI.MarkovSuperreflexivity.walkOrbitFraction line 15
  3. theorem OAI.MarkovSuperreflexivity.wordMap_displacement_lt_of_length_le line 18
  4. theorem OAI.MarkovSuperreflexivity.wordMap_symm_displacement_lt_of_length_le line 29
  5. theorem OAI.MarkovSuperreflexivity.pullbackPoint_displacement_lt line 35
  6. theorem OAI.MarkovSuperreflexivity.walkOrbitFloor_bounds line 42
  7. theorem OAI.MarkovSuperreflexivity.walkOrbitFraction_bounds line 49
  8. theorem OAI.MarkovSuperreflexivity.walkOrbitFraction_add_int line 54
  9. theorem OAI.MarkovSuperreflexivity.pullbackPoint_integer_mem line 60
  10. theorem OAI.MarkovSuperreflexivity.pullbackPoint_fraction_mem line 72
  11. theorem OAI.MarkovSuperreflexivity.pullbackPoint_integer_window line 87
  12. theorem OAI.MarkovSuperreflexivity.pullbackPoint_fraction_window line 97
  13. def OAI.MarkovSuperreflexivity.chartCut line 110
  14. theorem OAI.MarkovSuperreflexivity.chartCut_pos line 113
  15. theorem OAI.MarkovSuperreflexivity.chartCut_le line 116
  16. theorem OAI.MarkovSuperreflexivity.chartCut_lt_of_lt line 119
  17. theorem OAI.MarkovSuperreflexivity.chartCut_lt_bound_of_lt line 123
  18. theorem OAI.MarkovSuperreflexivity.chart_good_path_rank line 127
  19. theorem OAI.MarkovSuperreflexivity.chart_good_path_cut line 147
  20. theorem OAI.MarkovSuperreflexivity.pullbackPoint_good_path_cut line 158