OAI/Probability/SLE/Geometry/MarkedTubeLocalSides.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Uniform small physical tube neighbourhoods depart on opposite local sides of the marked corner. Openness determines either orientation of the actual conformal map-out; no boundary-order assertion is assumed.

  1. lemma OAI.SLEExactGauge.Serpentine.markedLeftRoute_small_time line 17
  2. lemma OAI.SLEExactGauge.Serpentine.markedRightRoute_small_time line 21
  3. lemma OAI.SLEExactGauge.Serpentine.marked_small_route_dist line 26
  4. lemma OAI.SLEExactGauge.Serpentine.marked_small_tube_coordinate line 43
  5. lemma OAI.SLEExactGauge.Serpentine.marked_small_tube_positive line 56
  6. lemma OAI.SLEExactGauge.Serpentine.marked_small_tube_negative line 67
  7. theorem OAI.SLEExactGauge.Serpentine.marked_physical_tubes_opposite_sides line 82