OAI/Probability/SLE/Mass/WaypointHarmonicMeasure.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The actual two-sided physical route events bound the two half-plane exit arcs from below. Uniform route support is proved elsewhere; only the generic published conformal Brownian exit law is parameterized here.

  1. theorem OAI.SLEExactGauge.RibbonCoordinates.finite_exit_event_measure_le_arc line 18
  2. theorem OAI.SLEExactGauge.RibbonCoordinates.ribbon_tube_harmonic_bounds line 48