OAI/Probability/SLE/Loewner/RealCharacteristicAvoidance.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Both signs of a noncolliding real characteristic give stable trace avoidance. A continuous real characteristic cannot change sides of the driver without colliding with it.

  1. lemma OAI.SLEExactGauge.StableTraceAvoidance.of_mirror line 14
  2. lemma OAI.SLEExactGauge.real_characteristic_one_side line 30
  3. theorem OAI.SLEExactGauge.stableTraceAvoidance_of_real_characteristic line 47