OAI/Probability/SLE/Geometry/RootExteriorChart.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The odd-root transform produces an actual exterior univalent map. Its first Laurent coefficient is the negative derivative of the root factor; the remainder is represented by a holomorphic disk function.

  1. def OAI.SLEExactGauge.rootExteriorChart line 14
  2. lemma OAI.SLEExactGauge.root_exterior_laurent_data line 16
  3. lemma OAI.SLEExactGauge.root_exterior_univalent line 56