OAI/Probability/FirstPassage/Waypoints.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PlanarFPP.segmentPoint line 9
2. def OAI.PlanarFPP.waypoint line 12
3. def OAI.PlanarFPP.SegmentTube line 15
4. theorem OAI.PlanarFPP.waypoint_zero line 18
5. theorem OAI.PlanarFPP.waypoint_end line 21
6. theorem OAI.PlanarFPP.waypoint_error line 25
7. theorem OAI.PlanarFPP.waypoint_displacement_error line 29
8. theorem OAI.PlanarFPP.waypoint_displacement_norm line 44
9. theorem OAI.PlanarFPP.waypoint_cost_bound line 59
10. theorem OAI.PlanarFPP.waypoint_ball_in_tube line 74
11. theorem OAI.PlanarFPP.mem_segmentTube_iff line 87