InteriorVisit.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

A positive bounded interior visit, obtained from the already proved sausage seed. This supplies the nondegeneracy event in the access-guide argument without a uniform support assumption.

theorem OAI.SLEExactGauge.RegularSLEPresentation.positive_bounded_interior_visit line 16

theorem OAI.SLEExactGauge.uniform_access_radius_lower_bound_of_interior_visit line 81

Source documentation

Localization only needs an interior visit before the bounded time, not a visit at a predetermined terminal time.

theorem uniform_access_radius_lower_bound_of_interior_visit
    {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω) [IsProbabilityMeasure P]
    (κ : ℝ) (hκ : 0 < κ) (hκ8 : κ < 8)
    (γ : Ω → ℝ≥0 → ℂ) (hSLE : IsOrdinaryChordalSLE κ γ P)
    (T : ℝ≥0) (R : ℝ) (Q : Set ℂ) (hQ : Q ⊆ upperHalfPlane)
    (hvisit : 0 < P {ω | (∀ t ∈ Icc 0 T, ‖γ ω t‖ < R) ∧
      ∃ t ∈ Icc 0 T, γ ω t ∈ Q})
    (r₀ : ℝ) (hr₀ : 0 < r₀) :
    ∃ rmin : ℝ, 0 < rmin ∧
      ∀ (F : ℂ → ℂ) (Fbar : ℂ → OnePoint ℂ),
      DifferentiableOn ℂ F upperHalfPlane → InjOn F upperHalfPlane →
      ContinuousOn Fbar {z : ℂ | 0 ≤ z.im} →
…

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