OAI/Probability/LatticePassage/PassageRegularity.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.CompanionFPP.measurable_pathCost line 10
2. instance OAI.CompanionFPP.countable_lattice_walk line 16
3. theorem OAI.CompanionFPP.measurable_passageTime line 20
4. theorem OAI.CompanionFPP.trail_positive_moment line 24
5. theorem OAI.CompanionFPP.passageTime_positive_moment line 39
6. theorem OAI.CompanionFPP.integrable_exp_passageTime line 54
7. theorem OAI.CompanionFPP.integrable_passageTime line 60
8. theorem OAI.CompanionFPP.passageTime_upper_tail line 70