OAI/Probability/SLE/Geometry/UnitWindowPlanarExit.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The exact deterministic rescaling between the published unit-window exit events and the original planar Wiener process.

  1. def OAI.SLEExactGauge.unitWindowStop line 16
  2. lemma OAI.SLEExactGauge.unitWindowStop_coe line 18
  3. lemma OAI.SLEExactGauge.unitWindowStop_bounds line 21
  4. lemma OAI.SLEExactGauge.physicalUnitBrownianPath_at_scale line 31
  5. lemma OAI.SLEExactGauge.physicalUnitBrownianPath_eq_planar line 43
  6. lemma OAI.SLEExactGauge.unitWindowFirstExit_planar line 53
  7. lemma OAI.SLEExactGauge.unitWindow_map_limit_iff line 69