OAI/Probability/SLE/Geometry/ActualCompactAvoidance.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Positive probability of preserving a compact surviving set of a prescribed continuous Loewner driver. This controls compact interior obstacles in the geometric-support construction.

  1. theorem OAI.SLEExactGauge.regular_scaled_driver_tube_positive line 16
  2. theorem OAI.SLEExactGauge.regular_compact_survival_positive line 38
  3. theorem OAI.SLEExactGauge.ordinary_compact_survival_positive line 54