OAI/Probability/SLE/Geometry/HalfPlaneExteriorConnected.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

A common connected exterior for every bounded half-plane obstacle. This lets unbounded complementary components be identified without any boundary regularity or choice of a conformal map.

  1. def OAI.SLEExactGauge.halfPlaneRectangleExterior line 14
  2. lemma OAI.SLEExactGauge.halfPlaneRectangleExterior_connected line 17
  3. lemma OAI.SLEExactGauge.mem_halfPlaneRectangleExterior_of_norm_lt line 53
  4. lemma OAI.SLEExactGauge.halfPlaneRectangleExterior_disjoint_bounded line 63
  5. theorem OAI.SLEExactGauge.halfPlane_complement_connected_of_unbounded_components line 73