OAI/Probability/SLE/Loewner/RawSurvivingAnalytic.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The raw surviving set is an open conformal image of the half-plane. For a smooth driver its radial tip lies on the boundary of this set.

  1. lemma OAI.SLEExactGauge.Target.surviving_eq_inverse_image line 15
  2. lemma OAI.SLEExactGauge.RegularSLEPresentation.raw_surviving_isOpen line 28
  3. lemma OAI.SLEExactGauge.RegularSLEPresentation.raw_forward_holomorphic line 37
  4. theorem OAI.SLEExactGauge.RegularSLEPresentation.smooth_raw_tip_not_surviving line 43