OAI/Analysis/MarkovType/WalkPrefixLevels.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MarkovSuperreflexivity.rawChartWalkSum line 13
  2. theorem OAI.MarkovSuperreflexivity.rawChartWalkSum_supportedBelow line 17
  3. theorem OAI.MarkovSuperreflexivity.rawChartWalkSum_prefix_bound line 25
  4. theorem OAI.MarkovSuperreflexivity.rawChartWalkSum_prefix_cocycle line 32
  5. def OAI.MarkovSuperreflexivity.walkIntegerPoint line 56
  6. def OAI.MarkovSuperreflexivity.walkFractionPoint line 61
  7. theorem OAI.MarkovSuperreflexivity.rawChartWalkSum_lower_level line 69
  8. theorem OAI.MarkovSuperreflexivity.rawChartWalkSum_upper_level line 89