FirstFrontPassage.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The retained endpoint and pre-front margins give an actual first-front stopping time, with the retained middle interval strictly before it.

def OAI.SLEExactGauge.FirstFrontPassage.firstFrontTime line 16
Source documentation
First time a scalar progress coordinate reaches the front.
```
def firstFrontTime (x : ℝ≥0 → ℝ) (q : ℝ) : WithTop ℝ≥0 :=
…
```
def OAI.SLEExactGauge.FirstFrontPassage.frontTime line 21
Source documentation
Finite-valued representative; it agrees with the actual first-front hitting time whenever a retained endpoint witnesses a crossing.
```
def frontTime (x : ℝ≥0 → ℝ) (q : ℝ) : ℝ≥0 :=
…
```
theorem OAI.SLEExactGauge.FirstFrontPassage.firstFrontTime_isStoppingTime line 24
theorem OAI.SLEExactGauge.FirstFrontPassage.exists_first_front line 34
Source documentation
A continuous crossing before a finite endpoint makes the infimum defining the stopping time an actual least crossing, even without global continuity.
```
theorem exists_first_front
    (x : ℝ≥0 → ℝ) (q : ℝ) (T : ℝ≥0)
    (hc : ContinuousOn x (Icc 0 T)) (hstart : x 0 < q) (hend : q < x T) :
    ∃ τ : ℝ≥0, firstFrontTime x q = (τ : WithTop ℝ≥0) ∧
      0 < τ ∧ τ < T ∧ x τ = q ∧ ∀ t < τ, x t < q := by
…
```
Mentions: OAI.SLEExactGauge.FirstFrontPassage.firstFrontTime

theorem OAI.SLEExactGauge.FirstFrontPassage.frontTime_between line 72

Source documentation

Early containment and a retained pre-front prefix force the actual first front stop to fall strictly after the retained middle interval.

theorem frontTime_between
    (x : ℝ≥0 → ℝ) (q : ℝ) (σ b T : ℝ≥0) (_hσb : σ ≤ b) (_hbT : b < T)
    (hc : ContinuousOn x (Icc 0 T))
    (hearly : ∀ t ∈ Icc 0 σ, x t < q)
    (hprefix : ∀ t ∈ Icc σ b, x t < q) (hend : q < x T) :
    firstFrontTime x q = (frontTime x q : WithTop ℝ≥0) ∧
      b < frontTime x q ∧ frontTime x q < T ∧ x (frontTime x q) = q := by
…

Mentions: OAI.SLEExactGauge.FirstFrontPassage.firstFrontTime, OAI.SLEExactGauge.FirstFrontPassage.frontTime

theorem OAI.SLEExactGauge.FirstFrontPassage.eventually_front_lt_on_compact_image line 94

Source documentation

Lower endpoint margins transfer by the same compact uniform-convergence argument as upper pre-front margins.

theorem eventually_front_lt_on_compact_image
    (Fₙ : ℕ → ℂ → ℂ) (F : ℂ → ℂ)
    (hF : ContinuousOn F upperHalfPlane)
    (hFconv : TendstoLocallyUniformlyOn Fₙ F atTop upperHalfPlane)
    (pₙ : ℕ → ℂ → ℝ) (p : ℂ → ℝ) (U : Set ℂ) (hU : IsOpen U)
    (hp : ContinuousOn p U) (hpconv : TendstoLocallyUniformlyOn pₙ p atTop U)
    (K : Set ℂ) (hK : IsCompact K) (hKH : K ⊆ upperHalfPlane)
    (hKU : F '' K ⊆ U) (q : ℝ) (hbound : ∀ z ∈ K, q < p (F z)) :
    ∀ᶠ n in atTop, ∀ z ∈ K, q < pₙ n (Fₙ n z) := by
…

Mentions: OAI.SLEExactGauge.upperHalfPlane

theorem OAI.SLEExactGauge.FirstFrontPassage.retained_tube_firstFront_sausage_mass line 113

Source documentation

Retained endpoint margins construct the actual finite first-front stop. The positive stopped sausage bound therefore needs no assumed front-stop fact.

theorem retained_tube_firstFront_sausage_mass
    {Ω : Type*} [MeasurableSpace Ω] (P : Measure Ω) [IsProbabilityMeasure P]
    (κ : ℝ) (hκ : 0 < κ) (hκ8 : κ < 8)
    (f : Ω → C(ℝ≥0, ℂ)) (hf : Measurable f)
    (hSLE : IsOrdinaryChordalSLE κ (fun ω => f ω) P)
    (σ : Ω → ℝ≥0) (hσ : Measurable σ)
    (Fₙ : ℕ → ℂ → ℂ) (F : ℂ → ℂ)
    (hFn : ∀ n, DifferentiableOn ℂ (Fₙ n) upperHalfPlane)
    (hinj : ∀ n, InjOn (Fₙ n) upperHalfPlane)
    (hF : DifferentiableOn ℂ F upperHalfPlane)
    (hne : ∀ z ∈ upperHalfPlane, deriv F z ≠ 0)
    (hconv : TendstoLocallyUniformlyOn Fₙ F atTop upperHalfPlane)
…

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