OAI/Probability/SLE/Loewner/SmoothRawTipLimit.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The exact raw inverse has a finite radial tip limit on a short smooth-driver interval. No geometric witness is assumed.

  1. lemma OAI.SLEExactGauge.exists_right_limit_of_complex_lipschitz line 13
  2. theorem OAI.SLEExactGauge.Target.inverseFlow_tip_limit_of_short_smooth_driver line 47