OAI/Probability/SLE/Gauge/UniformActualRibbonPassage.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Uniform one-step passage for actual ribbon histories. The two-sided waypoint angle and the compactness hypotheses are derived from the fixed patch bounds, the actual first-front past, and the published analytic and probabilistic inputs.

  1. structure OAI.SLEExactGauge.RibbonHistory line 20

    Source documentation

    Data at an actual attained ribbon front, before any restart.

    structure RibbonHistory (C L : ℝ≥0) (ε : ℝ) where
…
  2. def OAI.SLEExactGauge.RibbonHistory.guide line 50
  3. def OAI.SLEExactGauge.RibbonHistory.recenteredChart line 53
  4. theorem OAI.SLEExactGauge.uniform_actual_ribbon_passage line 57