OAI/Analysis/MarkovType/WalkLabels.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MarkovSuperreflexivity.walkAlphaPoint line 15
  2. def OAI.MarkovSuperreflexivity.walkBetaPoint line 19
  3. def OAI.MarkovSuperreflexivity.positiveWalkLabel line 23
  4. def OAI.MarkovSuperreflexivity.rawWalkLabel line 28
  5. theorem OAI.MarkovSuperreflexivity.rawWalkLabel_odd line 32
  6. theorem OAI.MarkovSuperreflexivity.walkEndpoint_rank_pair line 37
  7. theorem OAI.MarkovSuperreflexivity.walkEndpoint_rank_next line 45
  8. theorem OAI.MarkovSuperreflexivity.positiveWalkLabel_norm line 54
  9. theorem OAI.MarkovSuperreflexivity.rawWalkLabel_norm line 62
  10. theorem OAI.MarkovSuperreflexivity.rawWalkLabel_norm_pos line 69
  11. theorem OAI.MarkovSuperreflexivity.positiveWalkLabel_supportedBelow line 76
  12. theorem OAI.MarkovSuperreflexivity.rawWalkLabel_supportedBelow line 90
  13. theorem OAI.MarkovSuperreflexivity.rawWalkLabel_support_subset line 99
  14. theorem OAI.MarkovSuperreflexivity.positiveWalkLabel_prefix_bound line 108
  15. theorem OAI.MarkovSuperreflexivity.rawWalkLabel_prefix_bound line 118
  16. theorem OAI.MarkovSuperreflexivity.rawWalkLabel_total_zero line 125
  17. theorem OAI.MarkovSuperreflexivity.positiveWalkLabel_prefix line 139
  18. theorem OAI.MarkovSuperreflexivity.positiveWalkLabel_prefix_indicator line 153
  19. theorem OAI.MarkovSuperreflexivity.rawWalkLabel_prefix_eq_chi line 170