OAI/Probability/SLE/Geometry/MarkedRouteClearance.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Fixed positive clearance of both marked-point routes from the past and from the complete polygonal hook, away from their common initial point.

  1. lemma OAI.SLEExactGauge.Serpentine.markedHook_re_bounds line 14
  2. lemma OAI.SLEExactGauge.Serpentine.markedHook_im_lower line 27
  3. lemma OAI.SLEExactGauge.Serpentine.markedLeftRoute_before_two line 40
  4. lemma OAI.SLEExactGauge.Serpentine.markedLeftRoute_after_two line 51
  5. lemma OAI.SLEExactGauge.Serpentine.markedRightRoute_before_two line 56
  6. lemma OAI.SLEExactGauge.Serpentine.markedRightRoute_middle line 66
  7. lemma OAI.SLEExactGauge.Serpentine.markedRightRoute_after_three line 77
  8. theorem OAI.SLEExactGauge.Serpentine.markedRoutes_past_clearance line 85

    Source documentation

    The explicit routes are uniformly separated from every admissible past point, including before the local departure from the marked point.

    theorem markedRoutes_past_clearance {w q : ℂ} {a t : ℝ}
    (hwr : -3 ≤ w.re) (hwr1 : w.re ≤ 1) (hwi1 : w.im ≤ 1)
    (ha : 0 ≤ a) (ha1 : a ≤ 1)
    (hqre : -2 ≤ q.re ∧ q.re ≤ 2) (hqim : q.im ≤ 2)
    (hq : q.im ≤ w.im - 2 * a ∨ w.re + 2 * a ≤ q.re) :
    a ≤ dist (markedLeftRoute w a t) q ∧ a ≤ dist (markedRightRoute w a t) q := by
…

    Mentions: OAI.SLEExactGauge.Serpentine.markedLeftRoute, OAI.SLEExactGauge.Serpentine.markedRightRoute

  9. lemma OAI.SLEExactGauge.Serpentine.markedLeftRoute_early_below line 116
  10. theorem OAI.SLEExactGauge.Serpentine.markedLeftRoute_hook_clearance line 125

    Source documentation

    The lower route avoids the complete hook after time 1/4.

    theorem markedLeftRoute_hook_clearance {w : ℂ} {R a t u : ℝ}
    (hwr : 0 ≤ w.re) (hwi : w.im < 2) (hR : w.re < R)
    (ha : 0 < a) (ha1 : a ≤ 1) (ht : 1 / 4 ≤ t) (hu : 0 ≤ u) :
    a / 4 ≤ dist (markedLeftRoute w a t) (markedHook w R 2 a u) := by
…

    Mentions: OAI.SLEExactGauge.Serpentine.markedLeftRoute, OAI.SLEExactGauge.Serpentine.markedHook

  11. lemma OAI.SLEExactGauge.Serpentine.markedRightRoute_first line 140
  12. lemma OAI.SLEExactGauge.Serpentine.markedRightRoute_second line 156
  13. theorem OAI.SLEExactGauge.Serpentine.markedRightRoute_hook_clearance line 170

    Source documentation

    The upper route runs in the gap between the two vertical legs, then above the horizontal top, and finally along the exterior line.

    theorem markedRightRoute_hook_clearance {w : ℂ} {R a t u : ℝ}
    (hwr1 : w.re ≤ 1) (hwi : w.im ≤ 1) (hR : w.re < R) (hR2 : R ≤ 2)
    (ha : 0 < a) (ha1 : a ≤ 1) (ht : 1 / 4 ≤ t) (hu : 0 ≤ u) :
    a / 8 ≤ dist (markedRightRoute w a t) (markedHook w R 2 a u) := by
…

    Mentions: OAI.SLEExactGauge.Serpentine.markedRightRoute, OAI.SLEExactGauge.Serpentine.markedHook