OAI/Probability/SLE/Geometry/ExteriorJoukowski.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The Joukowski chart from the upper half of the exterior disk to the half-plane. This is the final elementary chart in exterior slit normalization.

  1. def OAI.SLEExactGauge.exteriorUpperDisk line 13
  2. def OAI.SLEExactGauge.exteriorJoukowski line 15
  3. lemma OAI.SLEExactGauge.exteriorJoukowski_im line 17
  4. lemma OAI.SLEExactGauge.exteriorJoukowski_im_mul line 21
  5. lemma OAI.SLEExactGauge.exteriorJoukowski_mapsTo line 27
  6. lemma OAI.SLEExactGauge.exteriorJoukowski_injOn line 37
  7. lemma OAI.SLEExactGauge.exteriorJoukowski_surjOn line 58
  8. theorem OAI.SLEExactGauge.exteriorJoukowski_bijOn line 102
  9. theorem OAI.SLEExactGauge.exteriorJoukowski_differentiableOn line 106