RibbonFrontFreshness.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

First arrival at a ribbon front is fresh in the actual Loewner sense: the current tip survives every strictly earlier hull. This identifies the access prime end with the current driving point through the proved fresh-tip chart limit.

theorem OAI.SLEExactGauge.RibbonCoordinates.ribbon_front_tip_survives_prior line 17

theorem OAI.SLEExactGauge.RibbonCoordinates.IsCapacityTwoWitness.ribbon_front_chart_tendsto line 52

Source documentation

The actual capacity chart tends to the current driver along the surviving domain at a first ribbon front.

theorem IsCapacityTwoWitness.ribbon_front_chart_tendsto
    {U : ℝ≥0 → ℝ} {γ : ℝ≥0 → ℂ} {G F : ℝ≥0 → ℂ → ℂ}
    (hw : IsCapacityTwoWitness U γ G F) (hU : Continuous U)
    (P : ℂ → ℂ) (hP : ContinuousOn P closedRibbon) (hi : InjOn P closedRibbon)
    (hH : ∀ z ∈ closedRibbon, 0 < z.re → P z ∈ upperHalfPlane)
    (hescape : Tendsto (fun s : ℝ => ‖P (s : ℂ)‖) atTop atTop)
    (x : ℝ≥0 → ℂ) (T : ℝ≥0) (hT : 0 < T) (hx : ContinuousOn x (Icc 0 T))
    (hx0 : (x 0).re = 0) (hcoords : MapsTo x (Icc 0 T) closedRibbon)
    (hγ : EqOn γ (P ∘ x) (Icc 0 T))
    (hfront : ∀ t : ℝ≥0, t < T → (x t).re < (x T).re)
    (hinterior : |(x T).im| < 1) :
    Tendsto (G T) (𝓝[survivingDomain γ T] (γ T)) (𝓝 (U T : ℂ)) := by
…

Mentions: OAI.SLEExactGauge.IsCapacityTwoWitness, OAI.SLEExactGauge.RibbonCoordinates.closedRibbon, OAI.SLEExactGauge.upperHalfPlane, OAI.SLEExactGauge.survivingDomain