OAI/Probability/SLE/Geometry/DiskBoundaryRegion.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

The full circle and its two half-disk Jordan regions.

  1. lemma OAI.SLEExactGauge.diskLowerArc_continuous line 12
  2. lemma OAI.SLEExactGauge.diskLowerArc_injOn line 15
  3. lemma OAI.SLEExactGauge.diskLowerArc_zero line 19
  4. lemma OAI.SLEExactGauge.diskLowerArc_one line 22
  5. theorem OAI.SLEExactGauge.disk_circle_jordan line 25
  6. theorem OAI.SLEExactGauge.complexInside_unitDisk line 45
  7. def OAI.SLEExactGauge.openLowerDisk line 54
  8. def OAI.SLEExactGauge.closedLowerDisk line 55
  9. lemma OAI.SLEExactGauge.conj_image_openUpperDisk line 57
  10. lemma OAI.SLEExactGauge.conj_image_closedUpperDisk line 66
  11. lemma OAI.SLEExactGauge.openLowerDisk_closure line 75
  12. lemma OAI.SLEExactGauge.conj_image_diskDiameter line 81
  13. theorem OAI.SLEExactGauge.complexInside_lowerDisk line 90
  14. lemma OAI.SLEExactGauge.closed_halfDisks_union line 103
  15. lemma OAI.SLEExactGauge.closed_halfDisks_inter line 113