OAI/Probability/SLE/Geometry/ReflectedRiemannSymmetry.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The positive-real derivative normalization makes the conformal chart of a reflection-invariant domain commute with complex conjugation.

  1. theorem OAI.SLEExactGauge.normalized_riemann_chart_conj line 14
  2. lemma OAI.SLEExactGauge.reflectedArcSet_conj line 38
  3. lemma OAI.SLEExactGauge.invertedExterior_conj line 46