OAI/Probability/SLE/Geometry/MeasurableBoundaryRestart.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The actual stopped trace law with a past-measurable boundary chart. The identity holds at all future times, including boundary visits, for the same chart family used in random continuation events.

  1. theorem OAI.SLEExactGauge.source_measurable_boundary_restart line 16