OAI/Probability/SLE/Geometry/ActualFirstHeightSupport.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The narrow first-height support event is proved directly from the Brownian driver and the deterministic Loewner equation.

  1. theorem OAI.SLEExactGauge.regular_strip_rise_positive line 16
  2. theorem OAI.SLEExactGauge.regular_narrowRise_positive line 56
  3. theorem OAI.SLEExactGauge.ordinary_strip_rise_positive line 65
  4. theorem OAI.SLEExactGauge.ordinary_narrowRise_positive line 81
  5. theorem OAI.SLEExactGauge.ordinary_narrowFirstHeight_positive line 97