UniformAccessLocalization.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

A common access radius from the converging inverse guides. A fixed positive guide time has a nonzero limiting parameter value; all sufficiently late guides therefore cross one common radius while their physical images stay in the prescribed small ball. This supplies the actual uniform localization hypotheses used before the first-height restart.

theorem OAI.SLEExactGauge.common_access_guide_radius line 17

theorem OAI.SLEExactGauge.common_access_gives_firstHeight_localization line 58

Source documentation

The common guide radius feeds the already proved actual localization estimate for every late member of the conformal family.

theorem common_access_gives_firstHeight_localization
    (κ : ℝ) (hκ : 0 < κ) (hκ8 : κ < 8) :
    ∃ b C c L₀ : ℝ, 0 < b ∧ 0 < C ∧ 0 < c ∧ 1 < L₀ ∧
    ∀ (Ω : Type*) [MeasurableSpace Ω] (P : Measure Ω) [IsProbabilityMeasure P]
      (γ : Ω → ℝ≥0 → ℂ), IsOrdinaryChordalSLE κ γ P →
      (∀ ω, Continuous (γ ω)) → (∀ ω, γ ω 0 = 0) → (∀ ω t, 0 ≤ (γ ω t).im) →
    ∀ (F : ℕ → ℂ → ℂ) (Fbar : ℕ → ℂ → OnePoint ℂ),
      (∀ n, DifferentiableOn ℂ (F n) upperHalfPlane) →
      (∀ n, InjOn (F n) upperHalfPlane) →
      (∀ n, ContinuousOn (Fbar n) closedHalfPlane) →
      (∀ n z, z ∈ upperHalfPlane → Fbar n z = (F n z : OnePoint ℂ)) →
    ∀ (δ : ℝ), 0 < δ →
…

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