OAI/Probability/SLE/Geometry/MarkedRoutes.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

Two explicit finite routes from the marked point to the exterior real boundary. One goes below the marked hook and exits on the left; the other passes between its legs, above its top, and exits on the right.

  1. def OAI.SLEExactGauge.Serpentine.clippedVector line 17
  2. lemma OAI.SLEExactGauge.Serpentine.clippedVector_lipschitz line 20
  3. lemma OAI.SLEExactGauge.Serpentine.clippedVector_shift_lipschitz line 34
  4. def OAI.SLEExactGauge.Serpentine.markedLeftRoute line 40
  5. def OAI.SLEExactGauge.Serpentine.markedRightRoute line 45
  6. lemma OAI.SLEExactGauge.Serpentine.markedLeftRoute_re line 51
  7. lemma OAI.SLEExactGauge.Serpentine.markedLeftRoute_im line 56
  8. lemma OAI.SLEExactGauge.Serpentine.markedRightRoute_re line 62
  9. lemma OAI.SLEExactGauge.Serpentine.markedRightRoute_im line 68
  10. lemma OAI.SLEExactGauge.Serpentine.markedLeftRoute_zero line 74
  11. lemma OAI.SLEExactGauge.Serpentine.markedRightRoute_zero line 77
  12. lemma OAI.SLEExactGauge.Serpentine.markedLeftRoute_final line 80
  13. lemma OAI.SLEExactGauge.Serpentine.markedLeftRoute_four line 84
  14. lemma OAI.SLEExactGauge.Serpentine.markedRightRoute_final line 88
  15. lemma OAI.SLEExactGauge.Serpentine.markedLeftRoute_continuous line 92
  16. lemma OAI.SLEExactGauge.Serpentine.markedRightRoute_continuous line 97
  17. lemma OAI.SLEExactGauge.Serpentine.markedLeftRoute_lipschitz line 102
  18. lemma OAI.SLEExactGauge.Serpentine.markedRightRoute_lipschitz line 116