Documentation

BGW.Skorokhod.Vervaat

First minimum times for càdlàg paths #

The lower envelope of a path and its left limit attains the infimum, including at the endpoints. Its minimizing set is compact, so it has a first element.

References: W. Vervaat, A relation between Brownian bridge and Brownian excursion, Ann. Probab. 7 (1979); T. Duquesne, A limit theorem for the contour process of conditioned Galton–Watson trees, Ann. Probab. 31 (2003), §4; items C33–C34 of CLASSICAL_THEORY_INPUTS.md.

source
theorem BGW.Skorokhod.exists_min_leftLim {T : ℝ} (f : D T ℝ) (hT : 0 ≤ T) :
∃ (t : ↑(Set.Icc 0 T)), min (Function.leftLim (⇑f) t) (f t) = ⨅ (s : ↑(Set.Icc 0 T)), f s

A real càdlàg path on a nonempty compact interval attains its infimum as a value or as a left limit.

source
noncomputable def BGW.Skorokhod.vervaatTime (f : D 1 ℝ) :
↑(Set.Icc 0 1)

The first time at which a real càdlàg path on [0,1] attains its infimum, either as a value or as a left limit (with f (0-) = f 0); C33.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem BGW.Skorokhod.min_leftLim_vervaatTime (f : D 1 ℝ) :
    min (Function.leftLim (⇑f) (vervaatTime f)) (f (vervaatTime f)) = ⨅ (s : ↑(Set.Icc 0 1)), f s

    The infimum is attained at vervaatTime f, as a value or a left limit (C33).

    source
    theorem BGW.Skorokhod.vervaatTime_le (f : D 1 ℝ) {t : ↑(Set.Icc 0 1)} (ht : min (Function.leftLim (⇑f) t) (f t) = ⨅ (s : ↑(Set.Icc 0 1)), f s) :
    vervaatTime f ≤ t

    vervaatTime f is the first such time (C33).