OAI/Probability/SLE/Gauge/RibbonFrontStops.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

One globally continuous ribbon progress coordinate supplies all integer first-front stopping times. Their order is pathwise, including infinite failure times, and successful histories identify them exactly.

  1. lemma OAI.SLEExactGauge.firstFrontTime_mono_of_initial line 16
  2. def OAI.SLEExactGauge.ribbonFrontStop line 42
  3. lemma OAI.SLEExactGauge.ribbonFrontStop_stopping line 45
  4. lemma OAI.SLEExactGauge.ribbonFrontStop_monotone line 53
  5. lemma OAI.SLEExactGauge.RibbonHistory.global_frontStop_eq line 63

    Source documentation

    The global first front agrees with the actual time in a successful history, irrespective of the extension away from the physical ribbon.

    lemma RibbonHistory.global_frontStop_eq
    {C L : ℝ≥0} {ε : ℝ} (d : RibbonHistory C L ε) (g : C(ℂ, ℝ))
    (hg : ∀ z ∈ closedRibbon, g (d.chart z) = z.re) :
    firstFrontTime (fun t => g (d.trace t)) d.front = (d.time : WithTop ℝ≥0) := by
…

    Mentions: OAI.SLEExactGauge.RibbonHistory