RibbonLimitSplice.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The limiting coordinate guide supplies the actual small-circle splice, its open continuation region, and a target strictly beyond the next front.

def OAI.SLEExactGauge.RibbonCoordinates.limitingFrontTarget line 15
theorem OAI.SLEExactGauge.RibbonCoordinates.limitingFrontTarget_isOpen line 18

theorem OAI.SLEExactGauge.RibbonCoordinates.limiting_guide_splice_geometry line 27

Source documentation

No small-image or last-crossing hypothesis is needed for the limiting splice: both follow from the actual continuous inverse guide and its boundary value.

theorem limiting_guide_splice_geometry
    (F : ℂ → ℂ) (hF : DifferentiableOn ℂ F upperHalfPlane)
    (hi : InjOn F upperHalfPlane) (α β : ℝ → ℂ)
    (hα : ContinuousOn α (Icc 0 (3 / 2 : ℝ)))
    (hβ : ContinuousOn β (Icc 0 (3 / 2 : ℝ))) (hβ0 : β 0 = 0)
    (hβH : MapsTo β (Ioc 0 (3 / 2 : ℝ)) upperHalfPlane)
    (hrel : EqOn (F ∘ β) α (Ioc 0 (3 / 2 : ℝ)))
    (homit : α 0 ∉ F '' upperHalfPlane)
    (U : Set ℂ) (hU : IsOpen U) (p : ℂ → ℝ) (hp : ContinuousOn p U)
    (hαU : α '' Icc (0 : ℝ) (3 / 2) ⊆ U)
    (hprogress : ∀ t ∈ Icc (0 : ℝ) (3 / 2), p (α t) = t)
    (r m : ℝ) (hr : 0 < r) (hm : 0 < m) :
…

Mentions: OAI.SLEExactGauge.upperHalfPlane