GuideTipCollapse.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Uniform collapse at the initial tip of access guides. The local uniform limit is assumed here; the boundary collapse itself is proved using the existing SLE localization estimate and a positive sausage seed.

theorem OAI.SLEExactGauge.uniform_tip_modulus_of_eventually_uniform line 18

Source documentation

Finitely many initial continuous guides can be absorbed into a common modulus once the tail has one.

theorem uniform_tip_modulus_of_eventually_uniform
    (β : ℕ → ℝ → ℂ) (T : ℝ) (hT : 0 < T)
    (hβ : ∀ n, ContinuousOn (β n) (Icc 0 T)) (hβ0 : ∀ n, β n 0 = 0)
    (htail : ∀ ε : ℝ, 0 < ε → ∃ h : ℝ, 0 < h ∧ h ≤ T ∧
      ∀ᶠ n in atTop, ∀ t ∈ Icc 0 h, ‖β n t‖ < ε) :
    ∀ ε : ℝ, 0 < ε → ∃ h : ℝ, 0 < h ∧ h ≤ T ∧
      ∀ n t, t ∈ Icc 0 h → ‖β n t‖ < ε := by
…

lemma OAI.SLEExactGauge.seed_ball_subset_halfPlane line 48

theorem OAI.SLEExactGauge.exists_separated_seed_ball line 59

Source documentation

Of two disjoint interior seed balls, at least one omits a given value under an injective map. Compactness then gives a positive separation.

theorem exists_separated_seed_ball
    (F : ℂ → ℂ) (a : ℂ) (hF : ContinuousOn F upperHalfPlane)
    (hinj : InjOn F upperHalfPlane) :
    ∃ z : ℂ, 2 < z.im ∧ ∃ r₀ : ℝ, 0 < r₀ ∧
      ∀ w ∈ closedBall z 2, r₀ ≤ ‖F w - a‖ := by
…

Mentions: OAI.SLEExactGauge.upperHalfPlane

theorem OAI.SLEExactGauge.seed_ball_eventually_separated line 95

theorem OAI.SLEExactGauge.uniform_tip_collapse line 129

Source documentation

A locally convergent conformal family has a common tip modulus. The physical guides have only a Lipschitz bound at their initial point; no boundary modulus of continuity for the maps is assumed.

theorem uniform_tip_collapse
    {Ω : Type} [MeasurableSpace Ω] (P : Measure Ω) [IsProbabilityMeasure P]
    (κ : ℝ) (hκ : 0 < κ) (hκ8 : κ < 8)
    (γ : Ω → ℝ≥0 → ℂ) (hSLE : IsOrdinaryChordalSLE κ γ P)
    (Fₙ : ℕ → ℂ → ℂ) (Fbar : ℕ → ℂ → OnePoint ℂ) (F : ℂ → ℂ)
    (hFn : ∀ n, DifferentiableOn ℂ (Fₙ n) upperHalfPlane)
    (hinjn : ∀ n, InjOn (Fₙ n) upperHalfPlane)
    (hbar : ∀ n, ContinuousOn (Fbar n) {z : ℂ | 0 ≤ z.im})
    (hext : ∀ n z, z ∈ upperHalfPlane → Fbar n z = (Fₙ n z : OnePoint ℂ))
    (hconv : TendstoLocallyUniformlyOn Fₙ F atTop upperHalfPlane)
    (hF : ContinuousOn F upperHalfPlane) (hinj : InjOn F upperHalfPlane)
    (aₙ : ℕ → ℂ) (a : ℂ) (ha : Tendsto aₙ atTop (𝓝 a))
…

Mentions: OAI.SLEExactGauge.IsOrdinaryChordalSLE, OAI.SLEExactGauge.upperHalfPlane