OAI/Probability/SLE/Geometry/PolarBoundarySeparation.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

A small inverse semicircle, closed outside the image domain, traps its radial interior. All intersections and transversality are explicit.

  1. lemma OAI.SLEExactGauge.path_ofLine_hasStrictDerivAt line 14
  2. lemma OAI.SLEExactGauge.polar_point_injective line 22
  3. lemma OAI.SLEExactGauge.polar_arc_traps_radial_point line 38