OAI/Analysis/MarkovType/ChartPathProbability.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MarkovSuperreflexivity.FiniteWalkDrift.markedPath_eventMass_edge line 20
  2. theorem OAI.MarkovSuperreflexivity.FiniteWalkDrift.markedStationaryEdgeMass_sum line 28
  3. theorem OAI.MarkovSuperreflexivity.FiniteWalkDrift.markedPath_bad_step_mass_le line 33
  4. theorem OAI.MarkovSuperreflexivity.FiniteWalkDrift.markedProb_valid_and line 52
  5. abbrev OAI.MarkovSuperreflexivity.FiniteWalkDrift.ConcreteChartState line 66
  6. abbrev OAI.MarkovSuperreflexivity.FiniteWalkDrift.ConcreteChartEdge line 68
  7. def OAI.MarkovSuperreflexivity.FiniteWalkDrift.concreteChartChain line 71
  8. def OAI.MarkovSuperreflexivity.FiniteWalkDrift.concreteChartGood line 75
  9. def OAI.MarkovSuperreflexivity.FiniteWalkDrift.concreteChartGoodMass line 78
  10. def OAI.MarkovSuperreflexivity.FiniteWalkDrift.concreteChartPathLetters line 82
  11. def OAI.MarkovSuperreflexivity.FiniteWalkDrift.concreteChartTVBound line 86
  12. theorem OAI.MarkovSuperreflexivity.FiniteWalkDrift.concreteChartPath_uniform_letters line 93
  13. theorem OAI.MarkovSuperreflexivity.FiniteWalkDrift.concreteChartPath_word_mass line 102
  14. theorem OAI.MarkovSuperreflexivity.FiniteWalkDrift.concreteChartPath_bad_step_of_good_mass line 110
  15. theorem OAI.MarkovSuperreflexivity.FiniteWalkDrift.concreteChartPath_bad_step line 116
  16. theorem OAI.MarkovSuperreflexivity.FiniteWalkDrift.concreteChartPath_bad_union line 125
  17. theorem OAI.MarkovSuperreflexivity.FiniteWalkDrift.concreteChartPath_bad_union_tenth line 140
  18. theorem OAI.MarkovSuperreflexivity.FiniteWalkDrift.concreteChartPath_reducedLength_mean_ge line 147
  19. theorem OAI.MarkovSuperreflexivity.FiniteWalkDrift.concreteChartPath_tail_all_good_of_good_mass line 154
  20. theorem OAI.MarkovSuperreflexivity.FiniteWalkDrift.concreteChartPath_valid_tail_all_good_of_good_mass line 174
  21. theorem OAI.MarkovSuperreflexivity.FiniteWalkDrift.exists_concreteChartPath_valid_tail_all_good line 184
  22. theorem OAI.MarkovSuperreflexivity.FiniteWalkDrift.concreteChartPath_tail_all_good line 195
  23. theorem OAI.MarkovSuperreflexivity.FiniteWalkDrift.concreteChartPath_valid_tail_all_good line 215