OAI/Probability/SLE/Gauge/StoppedSplicePassage.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The actual semicircle splice gives conditional passage after a narrow first-height stop. The physical tube here is in the original parameter plane, so compact continuation prefixes stay strictly inside the half-plane and can subsequently be transported through a locally convergent family.

  1. def OAI.SLEExactGauge.parameterContinuationRegion line 17
  2. theorem OAI.SLEExactGauge.parameterContinuationRegion_isOpen line 20
  3. theorem OAI.SLEExactGauge.exists_physical_splice_route line 26
  4. theorem OAI.SLEExactGauge.conditional_stopped_splice_positive line 82