OAI/Probability/LatticePassage/Stationarity.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.CompanionFPP.latticeTranslation line 8
2. lemma OAI.CompanionFPP.latticeTranslation_apply line 16
3. def OAI.CompanionFPP.environmentTranslation line 18
4. theorem OAI.CompanionFPP.measurable_environmentTranslation line 21
5. theorem OAI.CompanionFPP.environmentTranslation_preserving line 26
6. lemma OAI.CompanionFPP.pathCost_map_translation line 39
7. lemma OAI.CompanionFPP.walk_map_iso_surjective line 49
8. theorem OAI.CompanionFPP.passageTime_translation line 62
9. theorem OAI.CompanionFPP.mean_passageTime_translation line 74
10. theorem OAI.CompanionFPP.mean_passageTime_subadditive line 83