OAI/Probability/SLE/Loewner/RadiusHalfPlaneHull.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The explicit normalized chart of an upper half disk. Comparing with this chart bounds the capacity of a small slit.

  1. def OAI.SLEExactGauge.exteriorUpperRadius line 13
  2. def OAI.SLEExactGauge.radiusHullMap line 15
  3. lemma OAI.SLEExactGauge.divide_radius_bijOn line 17
  4. lemma OAI.SLEExactGauge.radiusHullMap_bijOn line 39
  5. lemma OAI.SLEExactGauge.radiusHullMap_formula line 47
  6. lemma OAI.SLEExactGauge.radiusHullMap_differentiableOn line 54
  7. lemma OAI.SLEExactGauge.radiusHullMap_coefficient line 60