OAI/Probability/SLE/Geometry/ExteriorLaurent.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Removing the pole of the exterior slit chart at infinity gives its first two Laurent coefficients without choosing a power-series expansion.

  1. def OAI.SLEExactGauge.slitInfinityFactor line 14
  2. lemma OAI.SLEExactGauge.slitInfinityFactor_zero line 17
  3. lemma OAI.SLEExactGauge.slitInfinityFactor_analyticAt line 22
  4. lemma OAI.SLEExactGauge.slitInfinityFactor_reflection line 31
  5. lemma OAI.SLEExactGauge.slitInfinityFactor_identity line 38
  6. lemma OAI.SLEExactGauge.slitInfinityFactor_remainder line 46
  7. lemma OAI.SLEExactGauge.slitExteriorMap_laurent_limit line 69