OAI/Probability/SLE/Geometry/DiskSideRegionImages.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Each prescribed side extension transports the corresponding closed region.

  1. lemma OAI.SLEExactGauge.image_interval_of_agree line 11
  2. lemma OAI.SLEExactGauge.image_eq_self_of_fixed line 20
  3. theorem OAI.SLEExactGauge.disk_upper_region_image line 29
  4. theorem OAI.SLEExactGauge.disk_lower_region_image line 38