OAI/Probability/GammaPassage/Waypoints.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.GammaFPP.IntervalTravelBridge.segmentPoint line 10
2. def OAI.GammaFPP.IntervalTravelBridge.waypoint line 13
3. def OAI.GammaFPP.IntervalTravelBridge.SegmentTube line 16
4. theorem OAI.GammaFPP.IntervalTravelBridge.waypoint_zero line 19
5. theorem OAI.GammaFPP.IntervalTravelBridge.waypoint_end line 22
6. theorem OAI.GammaFPP.IntervalTravelBridge.waypoint_error line 26
7. theorem OAI.GammaFPP.IntervalTravelBridge.waypoint_displacement_error line 30
8. theorem OAI.GammaFPP.IntervalTravelBridge.waypoint_displacement_norm line 45
9. theorem OAI.GammaFPP.IntervalTravelBridge.waypoint_cost_bound line 58
10. theorem OAI.GammaFPP.IntervalTravelBridge.waypoint_ball_in_tube line 73
11. theorem OAI.GammaFPP.IntervalTravelBridge.mem_segmentTube_iff line 88

    Source documentation

    Exact connection between the tube predicate and the closed Euclidean segment used in cr:local-travel.

    theorem mem_segmentTube_iff (p q z : Vertex) (R : ℝ) :
        z ∈ SegmentTube p q R ↔ ∃ v ∈ segment ℝ (latticeEmbed p) (latticeEmbed q),
          ‖latticeEmbed z-v‖ ≤ R := by
    …

    Mentions: OAI.GammaFPP.IntervalTravelBridge.SegmentTube