OAI/Probability/SLE/Loewner/SmoothRawFreshness.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The smooth raw tip survives at every earlier time. The proof uses compactness of an intermediate reverse image, with a uniform positive height, and the raw inverse composition identity.

  1. theorem OAI.SLEExactGauge.Target.smooth_raw_tip_survives_short_past line 18