CrosscutExitSides.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

A nonzero real map-out limit has the sign selected before the first domain exit. This turns geometric guide avoidance into an actual exit-arc event, once the published conformal Brownian exit law is supplied.

theorem OAI.SLEExactGauge.CrosscutSides.real_exit_positive_of_straightened_prefix line 18
theorem OAI.SLEExactGauge.CrosscutSides.real_exit_negative_of_straightened_prefix line 29

theorem OAI.SLEExactGauge.CrosscutSides.positive_first_exit_belongs_to_arc line 42

Source documentation

The scalar straightened side coordinate has a fixed sign until exit because its zero set is precisely the complete guide.

theorem positive_first_exit_belongs_to_arc
    (D : Set ℂ) (g : ℂ → ℂ) (h : ℂ ≃ₜ ℂ)
    (hreal : ∀ x : ℝ, h (x : ℂ) = (x : ℂ))
    (hg : ContinuousOn g D) (ζ : ℝ → ℂ) (hc : Continuous ζ)
    {τ : ℝ} (hτ : UnitWindowFirstExit D ζ τ)
    (haτ : (1 / 4 : ℝ) < τ)
    (hn : ∀ t ∈ Ico (1 / 4 : ℝ) τ, (h (g (ζ t))).re ≠ 0)
    (hstart : 0 < (h (g (ζ (1 / 4)))).re)
    (x : ℝ) (hx : x ≠ 0)
    (hlim : Tendsto (fun t => g (ζ t)) (𝓝[<] τ) (𝓝 (x : ℂ))) : 0 < x := by
…

Mentions: OAI.SLEExactGauge.UnitWindowFirstExit

theorem OAI.SLEExactGauge.CrosscutSides.negative_first_exit_belongs_to_arc line 60