OAI/Probability/SLE/Geometry/RootExteriorCompact.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The exterior map has compact omitted set. This supplies the compact region used in the area proof of the second-coefficient estimate.

  1. lemma OAI.SLEExactGauge.univalent_image_isOpen line 13
  2. lemma OAI.SLEExactGauge.root_exterior_contains_far_points line 20
  3. lemma OAI.SLEExactGauge.root_exterior_omitted_isCompact line 51