OAI/Probability/SLE/Loewner/RawLifetimeTrace.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

A point lost by the smooth raw flow is exactly the trace tip at its finite lifetime. The reverse path is the forward path read backwards.

  1. theorem OAI.SLEExactGauge.Target.eq_trace_at_lifetime line 14