OAI/Probability/SLE/Geometry/ComplexEndpointLimit.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A bounded upper-half-plane path has a real endpoint limit when its continuous image has a limit and the corresponding boundary fiber has no interval.

  1. lemma OAI.SLEExactGauge.real_cluster_in_boundary_fiber line 14
  2. theorem OAI.SLEExactGauge.exists_complex_endpoint_limit line 28