OAI/Probability/SLE/Gauge/SerpentineMarkedRouteClearance.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The two exit routes avoid every point of the complete marked access guide by one uniform margin, including its distant initial prefix.

  1. lemma OAI.SLEExactGauge.Serpentine.terminalAccess_bounds line 15
  2. theorem OAI.SLEExactGauge.Serpentine.completeMarkedAccess_route_clearance line 30

    Source documentation

    A margin independent of the number of serpentine columns.

    theorem completeMarkedAccess_route_clearance {s : ℝ} (hs : 0 < s) (hs1 : s ≤ 1)
    (w : ℂ) (hw : s ≤ w.im) (hw1 : ‖w‖ ≤ 1) (hwr : 0 ≤ w.re)
    {m : ℕ} (hm : 0 < m) {x t u : ℝ} (hx : |x| ≤ 1) (ht : 1 / 64 ≤ t) (hu : 0 ≤ u) :
    (s / 20) / 1000 ≤ dist (markedLeftRoute w (s / 20) t) (completeMarkedAccess s w m x u) ∧
    (s / 20) / 1000 ≤ dist (markedRightRoute w (s / 20) t) (completeMarkedAccess s w m x u) := by
…

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