OAI/Probability/FirstPassage/ProbabilityFoundations.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.PlanarFPP.(instance at line 9) line 9
2. instance OAI.PlanarFPP.rateOneProbability line 17
3. def OAI.PlanarFPP.exponentialProductLaw line 20
4. theorem OAI.PlanarFPP.exponentialProductLaw_environment line 23
5. theorem OAI.PlanarFPP.rateOne_ae_positive line 31
6. theorem OAI.PlanarFPP.ExponentialEnvironment.ae_positive line 42
7. theorem OAI.PlanarFPP.measurable_pathCost line 51
8. theorem OAI.PlanarFPP.measurable_passageTime line 58
9. theorem OAI.PlanarFPP.measurableSet_strict_path_event line 67
10. theorem OAI.PlanarFPP.measurableSet_bounded_path_event line 81