OAI/Probability/SLE/Geometry/MarkedWindowRoutes.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Compress the four-leg marked routes into the finite Brownian exit window used by the published conformal exit law.

  1. def OAI.SLEExactGauge.Serpentine.markedWindowRoute line 16
  2. lemma OAI.SLEExactGauge.Serpentine.markedWindowRoute_zero line 19
  3. lemma OAI.SLEExactGauge.Serpentine.markedWindowRoute_small line 24
  4. lemma OAI.SLEExactGauge.Serpentine.markedWindowRoute_final line 29
  5. lemma OAI.SLEExactGauge.Serpentine.markedWindowRoute_lipschitz line 33
  6. theorem OAI.SLEExactGauge.Serpentine.uniform_marked_window_tube_probability line 50