OAI/Probability/SLE/Loewner/ActualRadiusStopsRegular.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

For a regular Brownian driver with an actual capacity witness at every sample, the literal geometric radius-level time is a stopping time. No modification on an exceptional set is needed.

  1. theorem OAI.SLEExactGauge.actual_radiusLevelTime_stopping line 15
  2. lemma OAI.SLEExactGauge.actual_radiusLevelTime_past_mono line 45