OAI/Probability/SLE/Geometry/StableTraceAvoidance.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Local trace exclusions patch to an open tube by compactness. The bounded rectangle comes directly from the driver and capacity bounds.

  1. def OAI.SLEExactGauge.StableTraceAvoidance line 15
  2. lemma OAI.SLEExactGauge.stableTraceAvoidance_of_surviving line 20
  3. lemma OAI.SLEExactGauge.stableTraceAvoidance_of_real_trajectory line 37
  4. theorem OAI.SLEExactGauge.driver_neighborhood_trace_containment line 46