OAI/Probability/SLE/Geometry/DiskCrosscutBoundary.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The upper semicircle supplies the fixed boundary arc for the first relative Schoenflies extension of a compactified half-plane crosscut.

  1. def OAI.SLEExactGauge.diskUpperArc line 13
  2. lemma OAI.SLEExactGauge.diskUpperArc_continuous line 16
  3. lemma OAI.SLEExactGauge.diskUpperArc_zero line 20
  4. lemma OAI.SLEExactGauge.diskUpperArc_one line 21
  5. lemma OAI.SLEExactGauge.diskUpperArc_re line 23
  6. lemma OAI.SLEExactGauge.diskUpperArc_im line 28
  7. lemma OAI.SLEExactGauge.diskUpperArc_norm line 33
  8. lemma OAI.SLEExactGauge.diskUpperArc_injOn line 40
  9. lemma OAI.SLEExactGauge.disk_crosscut_meets_upper_at_endpoints line 49
  10. theorem OAI.SLEExactGauge.disk_crosscut_upper_jordan line 61