OAI/Probability/SLE/Geometry/HalfPlaneCayleyCompactification.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The fixed Cayley chart compactifies the closed upper half-plane by sending infinity to 1. It retains the real boundary pointwise as a parameterized unit circle, for the relative crosscut construction.

  1. def OAI.SLEExactGauge.halfPlaneCayley line 14
  2. lemma OAI.SLEExactGauge.halfPlaneCayley_den_ne line 16
  3. lemma OAI.SLEExactGauge.halfPlaneCayley_continuousOn line 22
  4. lemma OAI.SLEExactGauge.halfPlaneCayley_injOn line 27
  5. lemma OAI.SLEExactGauge.halfPlaneCayley_norm_le line 33
  6. lemma OAI.SLEExactGauge.halfPlaneCayley_norm_lt line 42
  7. lemma OAI.SLEExactGauge.halfPlaneCayley_real_norm line 51
  8. lemma OAI.SLEExactGauge.halfPlaneCayley_ne_one line 59
  9. lemma OAI.SLEExactGauge.halfPlaneCayley_zero line 66
  10. theorem OAI.SLEExactGauge.halfPlaneCayley_tendsto_infinity line 69