OAI/Probability/SLE/Geometry/HalfPlaneNormalizedUniqueness.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A normalized half-plane map with a normalized holomorphic inverse is the identity. The height comparison fixes its imaginary part, and the normalization removes the remaining real translation.

  1. theorem OAI.SLEExactGauge.normalized_halfPlane_left_inverse_eq_id line 15