OAI/Probability/SLE/Geometry/ConcatenatedSlitGeometry.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Geometric concatenation of an old simple slit and a fresh simple slit through its inverse chart. The resulting curve has no extra filled components.

  1. def OAI.SLEExactGauge.concatenateSlit line 14
  2. lemma OAI.SLEExactGauge.continuous_concatenateSlit line 17
  3. lemma OAI.SLEExactGauge.concatenateSlit_injective line 33
  4. lemma OAI.SLEExactGauge.concatenateSlit_positive line 63
  5. theorem OAI.SLEExactGauge.concatenateSlit_free_complement line 76