OAI/Probability/SLE/Loewner/SlitRealBoundaryFlow.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The exact capacity-clock real boundary coordinates are continuous, real valued and uniformly separated from the driver on a finite prefix.

  1. def OAI.SLEExactGauge.slitReflectedFlow line 14
  2. lemma OAI.SLEExactGauge.slitReflectedFlow_real_continuous line 19
  3. lemma OAI.SLEExactGauge.slitReflectedFlow_real line 26
  4. lemma OAI.SLEExactGauge.slitReflectedFlow_separated line 32
  5. theorem OAI.SLEExactGauge.slitReflectedFlow_uniform_limit line 41
  6. lemma OAI.SLEExactGauge.slitReflectedFlow_positive_gap line 57