OAI/Probability/LatticePassage/MeanTimeConstant.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CompanionFPP.meanPassageSequence line 9
2. lemma OAI.CompanionFPP.scaleVertex_add line 12
3. lemma OAI.CompanionFPP.meanPassageSequence_nonneg line 16
4. theorem OAI.CompanionFPP.meanPassageSequence_subadditive line 22
5. lemma OAI.CompanionFPP.meanPassageSequence_bddBelow line 29
6. def OAI.CompanionFPP.directionalMeanConstant line 35
7. theorem OAI.CompanionFPP.meanPassageSequence_tendsto line 38
8. theorem OAI.CompanionFPP.directionalMeanConstant_nonneg line 42
9. theorem OAI.CompanionFPP.directionalMeanConstant_le_mean line 46