SlitSupport.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The open-tube consequence of the SLE support theorem.

Tran–Yuan, A support theorem for SLE curves, Electron. J. Probab. 25 (2020), paper 18, Proposition 6.4 (printed page 18), as used in Theorem 1.1 and Corollary 1.2, DOI 10.1214/20-EJP425. Proposition 6.4 places every simple capacity-parametrized curve in the uniform support. Only positive probabilities of their uniform neighborhoods are assumed below; there is no uniform bound over curves or stopped pasts in this input.

def OAI.SLEExactGauge.PublishedSimpleTraceSupport line 23
Source documentation
The simple-curve inclusion in the published support theorem, restricted to finite deterministic capacity intervals.
```
def PublishedSimpleTraceSupport {Ω : Type*} [MeasurableSpace Ω]
    (P : Measure Ω) (γ : Ω → ℝ≥0 → ℂ) : Prop :=
…
```

theorem OAI.SLEExactGauge.slit_tube_support_of_published_support line 32

Source documentation

The pointwise support input yields the exact passage event used in the ribbon proof: containment in an open tube and a visit to the terminal target.

theorem slit_tube_support_of_published_support
    {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω)
    (γ : Ω → ℝ≥0 → ℂ) (hpublished : PublishedSimpleTraceSupport P γ)
    (T : ℝ≥0) (hT : 0 < T) (β : ℝ≥0 → ℂ) (U : ℝ≥0 → ℝ)
    (hU : Continuous U) (hβ : IsCapacityTwoTrace U β)
    (hinj : InjOn β (Icc 0 T)) (hinterior : ∀ t ∈ Ioc 0 T, β t ∈ upperHalfPlane)
    (N V : Set ℂ) (hN : IsOpen N) (hV : IsOpen V)
    (hsub : β '' Icc 0 T ⊆ N) (hend : β T ∈ V) :
    0 < P {ω | (∀ t ∈ Icc 0 T, γ ω t ∈ N) ∧ γ ω T ∈ V} := by
…

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