OAI/Probability/SLE/Gauge/ProperRibbonCoordinates.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

An escaping terminal straight piece makes the complete normal ribbon proper. Its inverse coordinates therefore extend continuously to the ambient plane, supplying one actual adapted front process for iteration.

  1. lemma OAI.SLEExactGauge.RibbonCoordinates.closedRibbon_isClosed line 16
  2. lemma OAI.SLEExactGauge.RibbonCoordinates.ribbon_coordinate_norm_bound line 20
  3. theorem OAI.SLEExactGauge.RibbonCoordinates.ribbon_closedEmbedding_of_linear_tail line 45
  4. lemma OAI.SLEExactGauge.RibbonCoordinates.coordinateInverse_continuousOn_of_embedding line 80
  5. theorem OAI.SLEExactGauge.RibbonCoordinates.exists_global_ribbon_progress line 94