OAI/Probability/SLE/Geometry/CompactifiedCrosscut.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

A proper half-plane ray becomes an injective compact disk crosscut from -1 to 1. The endpoint at infinity is filled by the proved Cayley limit, preserving the prescribed ray parameter.

  1. def OAI.SLEExactGauge.crosscutParameter line 14
  2. lemma OAI.SLEExactGauge.crosscutParameter_injectiveOn line 16
  3. lemma OAI.SLEExactGauge.crosscutParameter_continuousOn line 27
  4. lemma OAI.SLEExactGauge.crosscutParameter_tendsto line 32
  5. def OAI.SLEExactGauge.compactifiedCrosscut line 47
  6. lemma OAI.SLEExactGauge.compactifiedCrosscut_one line 50
  7. lemma OAI.SLEExactGauge.compactifiedCrosscut_eq line 53
  8. lemma OAI.SLEExactGauge.compactifiedCrosscut_zero line 57
  9. theorem OAI.SLEExactGauge.compactifiedCrosscut_properties line 62