OAI/Probability/FirstPassage/LocalTravel.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PlanarFPP.LocalTravel line 10
2. theorem OAI.PlanarFPP.localTravel_of_waypoint_tests line 14
3. theorem OAI.PlanarFPP.localTravel_parameters line 86
4. theorem OAI.PlanarFPP.localTravel_failure_bound line 140
5. theorem OAI.PlanarFPP.exponential_local_travel_nat line 168
6. theorem OAI.PlanarFPP.localTravel_mono line 185
7. theorem OAI.PlanarFPP.measurableSet_localTravel line 194
8. theorem OAI.PlanarFPP.exponential_local_travel line 208