OAI/Probability/SLE/Geometry/MarkedCornerChart.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

An explicit plane homeomorphism takes the real axis to the two legs of the marked access hook. It permits the same local crosscut argument as a smooth waypoint chart without smoothing the corner.

  1. def OAI.SLEExactGauge.Serpentine.cornerMap line 14
  2. def OAI.SLEExactGauge.Serpentine.cornerInv line 17
  3. lemma OAI.SLEExactGauge.Serpentine.cornerInv_cornerMap line 20
  4. lemma OAI.SLEExactGauge.Serpentine.cornerMap_cornerInv line 31
  5. def OAI.SLEExactGauge.Serpentine.markedCornerChart line 39
  6. lemma OAI.SLEExactGauge.Serpentine.markedCornerChart_zero line 52
  7. lemma OAI.SLEExactGauge.Serpentine.markedCornerChart_real_nonneg line 55
  8. lemma OAI.SLEExactGauge.Serpentine.markedCornerChart_real_nonpos line 59
  9. theorem OAI.SLEExactGauge.Serpentine.markedCornerChart_real_image line 63