OAI/Probability/SLE/Geometry/ActualWaypointAngle.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual uniform ribbon waypoint angle. Uniform Brownian route support, crosscut topology, and conformal Brownian exit bounds are the published inputs. The positive ribbon angle is derived here.

  1. theorem OAI.SLEExactGauge.RibbonCoordinates.uniform_actual_ribbon_waypoint_angle line 18