GuideInteriorSeparation.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

A fixed interior ball separated from the moving tip images in the guide compactness argument. Only local uniform convergence and continuity of the limit are used.

theorem OAI.SLEExactGauge.exists_interior_ball_eventually_separated line 19

Source documentation

A non-tip interior value of the limiting map supplies a fixed closed ball whose images stay uniformly away from the moving tip values.

theorem exists_interior_ball_eventually_separated
    (Fₙ : ℕ → ℂ → ℂ) (F : ℂ → ℂ) (aₙ : ℕ → ℂ) (a z₀ : ℂ)
    (hconv : TendstoLocallyUniformlyOn Fₙ F atTop upperHalfPlane)
    (ha : Tendsto aₙ atTop (𝓝 a)) (hF : ContinuousOn F upperHalfPlane)
    (hz₀ : z₀ ∈ upperHalfPlane) (hne : F z₀ ≠ a) :
    ∃ ρ r₀ : ℝ, 0 < ρ ∧ 0 < r₀ ∧ closedBall z₀ ρ ⊆ upperHalfPlane ∧
      ∀ᶠ n in atTop, ∀ z ∈ closedBall z₀ ρ, r₀ ≤ ‖Fₙ n z - aₙ n‖ := by
…

Mentions: OAI.SLEExactGauge.upperHalfPlane