OAI/Probability/SLE/Loewner/SmoothRawGeometry.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The raw smooth trace has the topology of a simple slit. Its raw surviving domain embeds in the geometric unbounded component; equality of these domains is treated separately.

  1. theorem OAI.SLEExactGauge.RegularSLEPresentation.smooth_raw_free_complement line 19
  2. theorem OAI.SLEExactGauge.RegularSLEPresentation.smooth_raw_surviving_subset_geometric line 34