OAI/Probability/SLE/Geometry/MarkedRouteSides.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The initial portions of the two physical routes lie on opposite sides of the explicit local corner chart.

  1. lemma OAI.SLEExactGauge.Serpentine.markedLeftRoute_corner_side line 15
  2. lemma OAI.SLEExactGauge.Serpentine.markedRightRoute_corner_side line 27