AccessGuideCollapse.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Uniform collapse of access guides from the already proved conformal localization estimate and pointwise slit support. An interior separated set prevents arbitrarily small physical images of a unit-modulus access guide.

theorem OAI.SLEExactGauge.uniform_access_image_radius_lower_bound line 16

theorem OAI.SLEExactGauge.no_shrinking_access_guides_of_published_support line 72

Source documentation

The separated interior set and published pointwise support rule out the bad sequence in the access-guide compactness argument. All map and guide conditions refer to the actual complex maps, rather than to an abstract state.

theorem no_shrinking_access_guides_of_published_support
    {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω) [IsProbabilityMeasure P]
    (κ : ℝ) (hκ : 0 < κ) (hκ8 : κ < 8)
    (γ : Ω → ℝ≥0 → ℂ) (hSLE : IsOrdinaryChordalSLE κ γ P)
    (hpublished : PublishedSimpleTraceSupport P γ)
    (T : ℝ≥0) (hT : 0 < T) (β : ℝ≥0 → ℂ) (U : ℝ≥0 → ℝ)
    (hU : Continuous U) (hβ : IsCapacityTwoTrace U β)
    (hinjβ : InjOn β (Icc 0 T)) (hβH : ∀ t ∈ Ioc 0 T, β t ∈ upperHalfPlane)
    (R : ℝ) (hβR : β '' Icc 0 T ⊆ ball 0 R)
    (Q : Set ℂ) (hQopen : IsOpen Q) (hQ : Q ⊆ upperHalfPlane) (hβQ : β T ∈ Q)
    (F : ℕ → ℂ → ℂ) (Fbar : ℕ → ℂ → OnePoint ℂ)
    (hF : ∀ n, DifferentiableOn ℂ (F n) upperHalfPlane)
…

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