OAI/Probability/SLE/Geometry/WaypointRoutes.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Explicit bounded-speed routes from the waypoint to either side of the core and then across it behind the front. These are the deterministic templates for the two Brownian tube events in the waypoint argument.

  1. def OAI.SLEExactGauge.RibbonCoordinates.unitClip line 18
  2. theorem OAI.SLEExactGauge.RibbonCoordinates.unitClip_lipschitz line 20
  3. theorem OAI.SLEExactGauge.RibbonCoordinates.unitClip_nonneg line 23
  4. theorem OAI.SLEExactGauge.RibbonCoordinates.unitClip_le_one line 25
  5. theorem OAI.SLEExactGauge.RibbonCoordinates.unitClip_of_nonpos line 28
  6. theorem OAI.SLEExactGauge.RibbonCoordinates.unitClip_of_one_le line 31
  7. theorem OAI.SLEExactGauge.RibbonCoordinates.unitClip_of_mem line 34
  8. def OAI.SLEExactGauge.RibbonCoordinates.waypointRoute line 37
  9. theorem OAI.SLEExactGauge.RibbonCoordinates.waypointRoute_re line 41
  10. theorem OAI.SLEExactGauge.RibbonCoordinates.waypointRoute_im line 45
  11. theorem OAI.SLEExactGauge.RibbonCoordinates.waypointRoute_zero line 49
  12. theorem OAI.SLEExactGauge.RibbonCoordinates.waypointRoute_continuous line 52
  13. theorem OAI.SLEExactGauge.RibbonCoordinates.waypointRoute_lipschitz line 57
  14. theorem OAI.SLEExactGauge.RibbonCoordinates.waypointRoute_im_bound line 84
  15. theorem OAI.SLEExactGauge.RibbonCoordinates.waypointRoute_mem_patch line 97
  16. theorem OAI.SLEExactGauge.RibbonCoordinates.waypointRoute_final_negative line 107

    Source documentation

    The final leg is the fixed transverse template, with one orientation for each side.

    theorem waypointRoute_final_negative (k : ℝ) {t : ℝ} (ht : t ∈ Icc (0 : ℝ) 1) :
    waypointRoute k (-1) (2 + t) = transverseTemplate k t := by
…

    Mentions: OAI.SLEExactGauge.RibbonCoordinates.waypointRoute

  17. theorem OAI.SLEExactGauge.RibbonCoordinates.waypointRoute_final_positive line 117