FirstHeightSupport.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

Positive probability of a narrow first-height crossing. The deterministic first crossing is finite, positive, fresh, and its entire past lies in the initial rectangle. A vertical supported path supplies the positive-probability event at each fixed spatial scale.

def OAI.SLEExactGauge.FirstHeightSupport.firstHeightTime line 21
Source documentation
The first capacity time at which the trace reaches the specified height.
```
def firstHeightTime (γ : ℝ≥0 → ℂ) (h : ℝ) : WithTop ℝ≥0 :=
…
```

theorem OAI.SLEExactGauge.FirstHeightSupport.firstHeightTime_isStoppingTime line 26

Source documentation

The actual first-height time is a stopping time for an adapted continuous trace.

theorem firstHeightTime_isStoppingTime
    {Ω : Type*} [m : MeasurableSpace Ω] (ℱ : Filtration ℝ≥0 m)
    (γ : Ω → ℝ≥0 → ℂ) (hγa : Adapted ℱ (fun t ω => γ ω t))
    (hγc : ∀ ω, Continuous (γ ω)) (h : ℝ) :
    IsStoppingTime ℱ (fun ω => firstHeightTime (γ ω) h) := by
…

Mentions: OAI.SLEExactGauge.FirstHeightSupport.firstHeightTime

theorem OAI.SLEExactGauge.FirstHeightSupport.exists_first_height line 39

Source documentation

A continuous trace which rises above a positive height has a genuine first crossing. Every earlier point has strictly smaller height.

theorem exists_first_height
    (γ : ℝ≥0 → ℂ) (hγ : Continuous γ) (hγ0 : γ 0 = 0)
    {h : ℝ} (hh : 0 < h) {T : ℝ≥0} (hT : h < (γ T).im) :
    ∃ τ : ℝ≥0, firstHeightTime γ h = (τ : WithTop ℝ≥0) ∧ 0 < τ ∧ τ < T ∧
      (γ τ).im = h ∧ ∀ u : ℝ≥0, u < τ → (γ u).im < h := by
…

Mentions: OAI.SLEExactGauge.FirstHeightSupport.firstHeightTime

def OAI.SLEExactGauge.FirstHeightSupport.narrowStrip line 83
def OAI.SLEExactGauge.FirstHeightSupport.aboveQuarterHeight line 85
def OAI.SLEExactGauge.FirstHeightSupport.narrowRiseEvent line 88
Source documentation
The measurable supported event used to obtain the narrow first crossing.
```
def narrowRiseEvent (B : ℝ) : Set C(ℝ≥0, ℂ) :=
…
```
theorem OAI.SLEExactGauge.FirstHeightSupport.isOpen_narrowRiseEvent line 91
theorem OAI.SLEExactGauge.FirstHeightSupport.measurableSet_narrowRiseEvent line 98
def OAI.SLEExactGauge.FirstHeightSupport.NarrowFirstHeight line 101
theorem OAI.SLEExactGauge.FirstHeightSupport.narrowRiseEvent_gives_first_height line 107
def OAI.SLEExactGauge.FirstHeightSupport.verticalPath line 126
Source documentation
A vertical reference path for the fixed-scale support event.
```
def verticalPath (B : ℝ) : Path (0 : ℂ) (((B / 2 : ℝ) : ℂ) * Complex.I) where
…
```
theorem OAI.SLEExactGauge.FirstHeightSupport.verticalPath_apply line 133
theorem OAI.SLEExactGauge.FirstHeightSupport.verticalPath_injective line 136
theorem OAI.SLEExactGauge.FirstHeightSupport.narrowRiseEvent_positive line 144
theorem OAI.SLEExactGauge.FirstHeightSupport.narrowFirstHeight_positive line 174
Source documentation
Ordinary SLE has positive probability of a finite positive first-height crossing with fresh tip and rectangle-contained past, at each fixed scale.
```
theorem narrowFirstHeight_positive
    {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω)
    (κ : ℝ) (γ : Ω → ℝ≥0 → ℂ) (hSLE : IsOrdinaryChordalSLE κ γ P)
    (hpublished : PublishedGeometricTubeSupport P γ) {B : ℝ} (hB : 0 < B) :
    0 < P {ω | NarrowFirstHeight B (γ ω)} := by
…
```
Mentions: OAI.SLEExactGauge.IsOrdinaryChordalSLE, OAI.SLEExactGauge.PublishedGeometricTubeSupport, OAI.SLEExactGauge.FirstHeightSupport.NarrowFirstHeight