OAI/Probability/SLE/Loewner/SmoothRawSimple.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Every positive-time raw tip is new: it survives all earlier times and fails to survive its own time. Hence the smooth raw trace is simple.

  1. lemma OAI.SLEExactGauge.Target.smooth_raw_tip_survives_past line 15
  2. theorem OAI.SLEExactGauge.RegularSLEPresentation.smooth_raw_trace_injective line 43