Terminal-window control for walk bridges

Reversing the bridge vector reduces terminal windows to initial windows. A single prefix density bound and the unconditioned small-block maximal estimate control them.

def BGW.StableTrees.DiscreteBridge.windowExceed {T : ℝ} (c r : ℝ) : Set (Skorokhod.D T ℝ)

The open exceedance event after a specified time on a càdlàg path.

Equations

• BGW.StableTrees.DiscreteBridge.windowExceed c r = {x : BGW.Skorokhod.D T ℝ | ∃ (t : ↑(Set.Icc 0 T)), c ≤ ↑t ∧ r < |x t|}

theorem BGW.StableTrees.DiscreteBridge.measurableSet_windowExceed {T c r : ℝ} (hc0 : 0 ≤ c) (hcT : c ≤ T) : MeasurableSet (windowExceed c r)

Open window exceedances are measurable by a countable detecting family of times.

theorem BGW.StableTrees.DiscreteBridge.walkBridgeLaw_terminal_le_prefix {μ : PMF ℕ} {B : ℕ → ℝ} {n : ℕ} (hn : Admissible μ n) (hB : 0 < B n) {ε δ : ℝ} (hε : 0 < ε) (hδ : 0 < δ) (hδhalf : 2 * δ < 1) (hnδ : 1 ≤ δ * ↑n) (hend : 1 / B n < ε / 4) : ↑(walkBridgeLaw μ B n hn) {x : Skorokhod.D 1 ℝ | ∃ (t : ↑(Set.Icc 0 1)), 1 - δ ≤ ↑t ∧ ε ≤ |x t|} ≤ ↑(restrictLaw ⟨2 * δ, ⋯⟩ ⋯ (walkBridgeLaw μ B n hn)) (windowExceed 0 (ε / 2))

A terminal window is bounded by an initial window of the reversed bridge vector.

theorem BGW.StableTrees.DiscreteBridge.walkBridgeLaw_terminal_small {μ : PMF ℕ} {θ : ℝ} {B : ℕ → ℝ} (h : StableDomain μ θ B) {q : ℕ → ℕ} (hqtop : Filter.Tendsto q Filter.atTop Filter.atTop) (hq : ∀ (k : ℕ), Admissible μ (q k)) {ε η : ℝ} (hε : 0 < ε) (hη : 0 < η) : ∃ (δ : ℝ), 0 < δ ∧ δ < 1 ∧ ∀ᶠ (k : ℕ) in Filter.atTop, ↑(walkBridgeLaw μ B (q k) ⋯) {x : Skorokhod.D 1 ℝ | ∃ (t : ↑(Set.Icc 0 1)), 1 - δ ≤ ↑t ∧ ε ≤ |x t|} ≤ ENNReal.ofReal η

Terminal window (time reversal of the bridge increments, endpoint error 1/B n): the walk bridge is uniformly small near time 1.