OAI/Probability/SLE/Loewner/InverseBoundaryClosingPath.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A small image semicircle can be closed by a small path outside the surviving domain. The closing path is supplied by the actual finite trace and real boundary, not by a further topological input.

  1. lemma OAI.SLEExactGauge.IsCapacityTwoWitness.exists_small_inverse_closing_path line 15