OAI/Probability/SLE/Geometry/NormalizedRiemannChart.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Normalization of the Riemann chart at the inversion origin. The phase is fixed by requiring a positive real first derivative.

  1. theorem OAI.SLEExactGauge.exists_zero_normalized_riemann_chart line 12