OAI/Probability/SLE/Loewner/SlitExteriorChart.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

The normalized reflected Riemann chart gives an analytic chart from an arbitrary simple attached slit domain onto the upper exterior disk.

  1. def OAI.SLEExactGauge.slitExteriorMap line 14
  2. lemma OAI.SLEExactGauge.inverse_mem_reflected_inverted line 16
  3. lemma OAI.SLEExactGauge.slitExteriorMap_eq_conjugate line 25
  4. lemma OAI.SLEExactGauge.slitExteriorMap_bijOn line 37
  5. lemma OAI.SLEExactGauge.slitExteriorMap_differentiableOn line 49
  6. theorem OAI.SLEExactGauge.simple_slit_exists_exterior_chart line 70