OAI/Probability/SLE/Geometry/PublishedBoundaryExtension.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A precise deterministic published input for boundary extensions. Rohde–Schramm, Basic properties of SLE, Annals of Mathematics 161 (2005), Theorem 4.1, pp. 898–899. A continuous Loewner driver whose tip limits form a continuous trace has inverse maps continuous on the closed half-plane. The input below keeps only this conclusion, composed with the continuous inclusion into the one-point compactification. It has no stochastic or uniform ribbon estimate.

  1. def OAI.SLEExactGauge.PublishedLoewnerBoundaryExtension line 19
  2. theorem OAI.SLEExactGauge.normalized_capacity_inverse_boundary_extension line 27