OAI/Probability/SLE/Geometry/RealSymmetricDiskMapSign.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The normalized chart preserves the upper side. Reflection excludes interior real values, and the positive derivative fixes the component sign.

  1. lemma OAI.SLEExactGauge.real_symmetric_injective_im_ne_zero line 14
  2. lemma OAI.SLEExactGauge.positive_derivative_upper_witness line 25
  3. theorem OAI.SLEExactGauge.normalized_riemann_maps_upper line 53