OAI/Probability/SLE/Geometry/PublishedConformalExitLaw.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Finite-window consequences of published conformal invariance of planar Brownian motion: G. F. Lawler, Conformally Invariant Processes in the Plane, AMS (2005), Theorem 2.2. The half-plane harmonic-measure formula is recorded in Lawler--Werness, Ann. Probab. 41 (2013), 1513--1555, §2.1, unnumbered display for S-hat (electronic reprint p. 5, DOI 10.1214/11-AOP695).

Only finite exits during one unit Brownian window are used. Time is deterministically rescaled from [0,1] to [0,3]. The input states actual map-out limits and exit-event upper bounds, with no ribbon hypotheses and no positive lower probability or angle estimate.

  1. def OAI.SLEExactGauge.UnitWindowFirstExit line 23
  2. def OAI.SLEExactGauge.unitWindowExitArc line 26
  3. def OAI.SLEExactGauge.PublishedHalfPlaneConformalExitLaw line 32