OAI/Probability/SLE/Loewner/SmoothRawDomain.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

For a smooth driver the raw survival domain is the geometric slit domain. Every lost interior point is a tip at its first lifetime.

  1. theorem OAI.SLEExactGauge.Target.exists_trace_time_of_not_surviving line 15
  2. theorem OAI.SLEExactGauge.Target.smooth_geometric_subset_raw_surviving line 29
  3. theorem OAI.SLEExactGauge.RegularSLEPresentation.smooth_raw_surviving_eq_geometric line 42