OAI/Probability/SLE/Geometry/OutwardRealBarrier.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A forward Loewner real coordinate outside the driver range moves outward. This elementary barrier also applies before a finite lifetime.

  1. lemma OAI.SLEExactGauge.outward_real_barrier line 12
  2. lemma OAI.SLEExactGauge.inward_negative_real_barrier line 30