OAI/Probability/SLE/Loewner/SmoothRawTipGlobal.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

A bounded derivative gives a finite radial tip limit at every time. The proof first gains a positive height on a short terminal interval, then uses ordinary interior stability for the remaining reverse time.

  1. theorem OAI.SLEExactGauge.Target.inverseFlow_vertical_distance_of_smooth_driver line 15
  2. theorem OAI.SLEExactGauge.Target.inverseFlow_tip_limit_of_smooth_window line 55
  3. lemma OAI.SLEExactGauge.Target.exists_smooth_window line 70
  4. theorem OAI.SLEExactGauge.Target.inverseFlow_tip_limit_of_smooth_driver line 79