OAI/Probability/SLE/Loewner/TraceDomainBoundary.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Every finite Loewner-domain boundary point is on the finite trace or on the real axis. This identifies the possible inverse cluster points.

  1. lemma OAI.SLEExactGauge.frontier_survivingDomain_subset line 13