GeometricTubeSupport.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

The clock-free open-tube specialization of the published support input.

Tran–Yuan (2020), A support theorem for SLE curves, Corollary 1.2 (strong topology, i.e. modulo increasing reparameterization). Its simple-curve inclusion, with the usual capacity normalization/dilation, gives the specialization below for a geometric simple path. Only positivity for each fixed tube is assumed; no uniformity over tubes or pasts is assumed.

def OAI.SLEExactGauge.pathTubeEvent line 24
theorem OAI.SLEExactGauge.isOpen_pathTubeEvent line 27
theorem OAI.SLEExactGauge.measurableSet_pathTubeEvent line 40
def OAI.SLEExactGauge.PublishedGeometricTubeSupport line 45
Source documentation
A precise small consequence of the simple-curve inclusion in Tran–Yuan, Corollary 1.2, suited to the actual geometric continuation route.
```
def PublishedGeometricTubeSupport {Ω : Type*} [MeasurableSpace Ω]
    (P : Measure Ω) (γ : Ω → ℝ≥0 → ℂ) : Prop :=
…
```

theorem OAI.SLEExactGauge.geometric_tube_passage_of_published_support line 54

Source documentation

The geometrically stated published input applies directly to the Borel passage event on continuous-path space.

theorem geometric_tube_passage_of_published_support
    {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω)
    (f : Ω → C(ℝ≥0, ℂ))
    (hpublished : PublishedGeometricTubeSupport P (fun ω => f ω))
    (z : ℂ) (p : Path (0 : ℂ) z) (hp : Function.Injective p)
    (hpH : ∀ t, t ≠ 0 → p t ∈ upperHalfPlane)
    (N V : Set ℂ) (hN : IsOpen N) (hV : IsOpen V)
    (hpN : range p ⊆ N) (hzV : z ∈ V) :
    0 < P (f ⁻¹' pathTubeEvent N V) :=
…

Mentions: OAI.SLEExactGauge.PublishedGeometricTubeSupport, OAI.SLEExactGauge.upperHalfPlane, OAI.SLEExactGauge.pathTubeEvent