OAI/Analysis/MarkovType/FiniteWalk.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MarkovSuperreflexivity.normalizedChartEdgeLabel line 18
2. theorem OAI.MarkovSuperreflexivity.normalizedChartEdgeLabel_odd line 22
3. theorem OAI.MarkovSuperreflexivity.normalizedChartEdgeLabel_unit line 32
4. theorem OAI.MarkovSuperreflexivity.normalizedChartEdgeLabel_supportedBelow line 41
5. theorem OAI.MarkovSuperreflexivity.normalizedChartEdgeSum_norm line 49
6. theorem OAI.MarkovSuperreflexivity.normalizedChartEdgeSum_displacement line 59
7. theorem OAI.MarkovSuperreflexivity.finiteWalk line 76