RibbonSideCorridors.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The two strips outside the narrow core are in the actual surviving component. Their connection to the unbounded future excludes filled hulls, even when the stopped past is not simple.

def OAI.SLEExactGauge.RibbonCoordinates.sideCorridor line 15
theorem OAI.SLEExactGauge.RibbonCoordinates.sideCorridor_convex line 18

theorem OAI.SLEExactGauge.RibbonCoordinates.sideCorridor_survives line 24

Source documentation

A strip strictly outside the past's core connects to the free future and hence is in the unbounded surviving domain. This covers either side.

theorem sideCorridor_survives
    (P : ℂ → ℂ) (hP : ContinuousOn P closedRibbon) (hi : InjOn P closedRibbon)
    (hH : ∀ z ∈ closedRibbon, 0 < z.re → P z ∈ upperHalfPlane)
    (γ : ℝ≥0 → ℂ) (T : ℝ≥0) {k ε a b : ℝ} (hk : 0 ≤ k)
    (hab : a < b) (ha : -1 ≤ a) (hb : b ≤ 1)
    (hgap : ∀ x ∈ Ioo a b, ε < |x|)
    (hpast : γ '' Icc 0 T ⊆
      P '' {z ∈ closedRibbon | z.re ≤ k ∧ |z.im| ≤ ε})
    (hunbounded : ¬ Bornology.IsBounded (P '' futureRibbon k)) :
    P '' sideCorridor a b ⊆ survivingDomain γ T := by
…

Mentions: OAI.SLEExactGauge.RibbonCoordinates.closedRibbon, OAI.SLEExactGauge.upperHalfPlane, OAI.SLEExactGauge.RibbonCoordinates.futureRibbon, OAI.SLEExactGauge.RibbonCoordinates.sideCorridor, OAI.SLEExactGauge.survivingDomain