OAI/Probability/SLE/Geometry/InvertedExterior.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Inverting a bounded obstacle and adding the point at infinity at zero. This is the domain used for conformal normalization at infinity.

  1. def OAI.SLEExactGauge.invertedExterior line 14
  2. lemma OAI.SLEExactGauge.invertedExterior_eq_insert line 16
  3. lemma OAI.SLEExactGauge.zero_mem_invertedExterior line 28
  4. lemma OAI.SLEExactGauge.invertedExterior_isOpen line 30
  5. lemma OAI.SLEExactGauge.zero_mem_closure_inverted_complement line 56
  6. theorem OAI.SLEExactGauge.invertedExterior_connected line 78