OAI/Probability/SLE/Geometry/ClosedArcCrossing.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Closing an arc by a path outside the domain preserves its unique interior crossing. This connects the small-loop obstruction to inverse Loewner semicircles.

  1. lemma OAI.SLEExactGauge.path_trans_first_strict_deriv line 14
  2. lemma OAI.SLEExactGauge.small_closed_arc_no_transverse_crossing line 24