Running infima under extraction clocks

Prefix infima obey the same uniform error bound as the paths under an increasing time change.

noncomputable def BGW.StableTrees.extractionPrefixInf {M : ℝ} (p : Skorokhod.D M ℝ) (t : ↑(Set.Icc 0 M)) : ℝ

The infimum of a finite-horizon path up to a time in its domain. Reference: Billingsley (1999), Chapter 3.

Equations

• BGW.StableTrees.extractionPrefixInf p t = ⨅ (s : ↑(Set.Iic t)), p ↑s

theorem BGW.StableTrees.extractionPrefixInf_aligned_le {M : ℝ} (p q : Skorokhod.D M ℝ) (σ : Skorokhod.TimeChange M) {ε : ℝ} (hε : ∀ (s : ↑(Set.Icc 0 M)), dist (p (σ s)) (q s) ≤ ε) (t : ↑(Set.Icc 0 M)) : |extractionPrefixInf p (σ t) - extractionPrefixInf q t| ≤ ε

An aligned uniform path error controls every prefix infimum. Reference: Billingsley (1999), Chapter 3.

theorem BGW.StableTrees.extractionPrefixInf_restrict (M : NNReal) (f : Skorokhod.DLoc) (t : ↑(Set.Icc 0 ↑M)) : extractionPrefixInf (Skorokhod.DLoc.restrict M f) t = runningInfLoc f ⟨↑t, ⋯⟩

Restricting a local path preserves prefix infima. Reference: Billingsley (1999), Chapter 3.

theorem BGW.StableTrees.extractionPrefixInf_at_ladderTime {M B : ℝ} {ω : ℕ → ℝ} {n r : ℕ} (hn : 0 < n) (hB : 0 < B) (hfin : walkHitTime r ω ≠ ⊤) (hM : ↑(ladderTime ω r) / ↑n ≤ M) : extractionPrefixInf (Skorokhod.realStepPath M n B ω) ⟨↑(ladderTime ω r) / ↑n, ⋯⟩ = Probability.RealWalk.partialSum ω (ladderTime ω r) / B

At a finite ladder time, the scaled path's prefix infimum is its current value. Reference: Billingsley (1999), Chapter 3.