OAI/Probability/SLE/Geometry/WaypointRouteAvoidance.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

After the initial free move, either waypoint route remains a fixed distance from the complete access guide. Embedded coordinate disks turn this into physical separation, including nonlocal pieces of the guide.

  1. theorem OAI.SLEExactGauge.RibbonCoordinates.waypointRoute_before_two_offset line 15
  2. theorem OAI.SLEExactGauge.RibbonCoordinates.waypointRoute_guide_separation line 25
  3. theorem OAI.SLEExactGauge.RibbonCoordinates.waypointRoute_ball_subset_patch line 49
  4. theorem OAI.SLEExactGauge.RibbonCoordinates.physical_waypointRoute_avoids_complete_guide line 68

    Source documentation

    Physical separation follows from the full ribbon embedding: a nonlocal guide point cannot enter the image of a local coordinate disk either.

    theorem physical_waypointRoute_avoids_complete_guide
    (hpublished : PublishedPlanarDiskOpenness)
    (P : ℂ → ℂ) (hP : ContinuousOn P closedRibbon) (hi : InjOn P closedRibbon)
    (K : ℝ≥0) (hK : 0 < (K : ℝ)) {k x side t u : ℝ}
    (hk : 1 ≤ k) (hx : |x| ≤ 1 / 16) (hside : |side| = 1)
    (hlower : ∀ v ∈ crossingPatch k, ∀ w ∈ crossingPatch k,
      dist v w ≤ K * dist (P v) (P w))
    (ht : 1 / 4 ≤ t) (hu : 0 ≤ u) :
    P (guideCoordinate k x u) ∉ ball (P (waypointRoute k side t)) ((1 / 32 : ℝ) / K) := by
…

    Mentions: OAI.SLEExactGauge.PublishedPlanarDiskOpenness, OAI.SLEExactGauge.RibbonCoordinates.closedRibbon, OAI.SLEExactGauge.RibbonCoordinates.crossingPatch, OAI.SLEExactGauge.RibbonCoordinates.guideCoordinate, OAI.SLEExactGauge.RibbonCoordinates.waypointRoute