Discrete Vervaat indices and step paths

Step paths include their terminal prefix sum. The discrete index is the first minimizer among the nonempty prefixes, as in Definition 6.3 of the source.

noncomputable def BGW.Skorokhod.stepPath (x : List ℤ) (B : ℝ) : D 1 ℝ

The step path t ↦ w_{⌊k t⌋} / B of a word x of length k, where w_j is the sum of the first j letters; its value at 1 is w_k / B (C33.5).

Equations

• BGW.Skorokhod.stepPath x B = { toFun := fun (t : ↑(Set.Icc 0 1)) => ↑(List.take ⌊↑x.length * ↑t⌋₊ x).sum / B, isCadlag' := ⋯ }

noncomputable def BGW.Skorokhod.vervaatIndex (x : List ℤ) : ℕ

The paper's discrete Vervaat index: the first i ∈ [1, k] at which the prefix sum w_i attains min_{1 ≤ j ≤ k} w_j (C33.5); 0 for the empty word.

Equations

• BGW.Skorokhod.vervaatIndex x = sInf {i : ℕ | 1 ≤ i ∧ i ≤ x.length ∧ ∀ (j : ℕ), 1 ≤ j → j ≤ x.length → (List.take i x).sum ≤ (List.take j x).sum}

theorem BGW.Skorokhod.vervaatTime_stepPath {x : List ℤ} (hx : ∃ (j : ℕ), 1 ≤ j ∧ j ≤ x.length ∧ (List.take j x).sum < 0) {B : ℝ} (hB : 0 < B) : ↑(vervaatTime (stepPath x B)) = ↑(vervaatIndex x) / ↑x.length

The minimizing time of a step path is the first minimizing prefix divided by the length.

theorem BGW.Skorokhod.vervaatD_stepPath {x : List ℤ} (hx : ∃ (j : ℕ), 1 ≤ j ∧ j ≤ x.length ∧ (List.take j x).sum < 0) {B : ℝ} (hB : 0 < B) : vervaatD (stepPath x B) = stepPath (x.rotate (vervaatIndex x)) B

Discrete correspondence: for a word whose prefix sums go below zero, the càdlàg Vervaat map of its step path is the step path of its rotation at the Vervaat index (C33.5).

theorem BGW.Skorokhod.isTreeExcursion_rotate_vervaatIndex {n : ℕ} {x : List ℤ} (hx : x ∈ bridgeWords n) : IsTreeExcursion (x.rotate (vervaatIndex x))

For a bridge word, the rotation at the Vervaat index is a tree excursion (C33.5, in the library's walk language).