OAI/Probability/SLE/Geometry/HalfPlaneJulia.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The boundary Schwarz–Pick limit at infinity. Only a normalized sequence tending vertically to infinity is needed for slit comparisons.

  1. lemma OAI.SLEExactGauge.normSq_div_real line 13
  2. lemma OAI.SLEExactGauge.halfPlane_schwarz_pick_scaled line 16
  3. theorem OAI.SLEExactGauge.halfPlane_julia_at_infinity line 38