Moving-time convergence of running infima

When the limiting running infimum is continuous, prefix infima converge at moving times.

theorem BGW.StableTrees.tendsto_extractionPrefixInf {M : NNReal} {p : ℕ → Skorokhod.D ↑M ℝ} {f : Skorokhod.DLoc} (hI : Continuous (runningInfLoc f)) (hp : Filter.Tendsto p Filter.atTop (nhds (Skorokhod.DLoc.restrict M f))) {t : ℕ → ↑(Set.Icc 0 ↑M)} {a : NNReal} (ht : Filter.Tendsto (fun (n : ℕ) => ↑(t n)) Filter.atTop (nhds ↑a)) : Filter.Tendsto (fun (n : ℕ) => extractionPrefixInf (p n) (t n)) Filter.atTop (nhds (runningInfLoc f a))

J1 convergence and a continuous limiting infimum permit moving evaluation times. Reference: Billingsley (1999), Chapter 3.