OAI/Probability/SLE/Geometry/MarkedAccessAngle.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The marked-point angle follows from the actual complete access guide, two uniformly supported Brownian routes and the cited conformal exit law. This isolates explicit physical geometry for the serpentine application.

  1. theorem OAI.SLEExactGauge.Serpentine.uniform_marked_access_angle line 20