OAI/Probability/SLE/Geometry/MarkedRouteEarlyClearance.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Uniform hook separation already at the early local-side test time.

  1. lemma OAI.SLEExactGauge.Serpentine.right_early_box line 13
  2. lemma OAI.SLEExactGauge.Serpentine.left_very_early_clearance line 30
  3. lemma OAI.SLEExactGauge.Serpentine.right_very_early_clearance line 43
  4. theorem OAI.SLEExactGauge.Serpentine.markedRoutes_hook_clearance_early line 67

    Source documentation

    A common margin for both routes from the local-side test onward.

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

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