Convergence of the contour from its strict prefixes

Constant extensions of height prefixes approximate the contour. Terminal-window control makes this approximation uniform in probability as the prefix tends to the whole interval.

noncomputable def BGW.StableTrees.ExactContour.extendPrefix (a : NNReal) (g : C(↑(Set.Icc 0 ↑a), ℝ)) : C(↑unitInterval, ℝ)

Extend a continuous prefix to the unit interval by its terminal value.

Equations

• BGW.StableTrees.ExactContour.extendPrefix a g = g.comp { toFun := fun (t : ↑unitInterval) => ⟨min ↑t ↑a, ⋯⟩, continuous_toFun := ⋯ }

theorem BGW.StableTrees.ExactContour.continuous_extendPrefix (a : NNReal) : Continuous (extendPrefix a)

Constant extension is continuous in the uniform topologies.

noncomputable def BGW.StableTrees.ExactContour.stopPrefix (a : NNReal) (ha : a ≤ 1) (g : C(↑unitInterval, ℝ)) : C(↑unitInterval, ℝ)

Stop a continuous unit-interval path at a prefix time.

Equations

• BGW.StableTrees.ExactContour.stopPrefix a ha g = BGW.StableTrees.ExactContour.extendPrefix a (g.comp { toFun := Set.inclusion ⋯, continuous_toFun := ⋯ })

theorem BGW.StableTrees.ExactContour.continuous_stopPrefix (a : NNReal) (ha : a ≤ 1) : Continuous (stopPrefix a ha)

Stopping at a fixed prefix time is continuous in the uniform topology.

theorem BGW.StableTrees.ExactContour.tendsto_exactContourLaw {μ : PMF ℕ} {θ : ℝ} {B : ℕ → ℝ} (h : StableDomain μ θ B) {q : ℕ → ℕ} (hqtop : Filter.Tendsto q Filter.atTop Filter.atTop) (hq : ∀ (k : ℕ), Admissible μ (q k)) : Filter.Tendsto (fun (k : ℕ) => (DiscreteForest.exactTreeLaw μ (q k)).map (treeContourPath B (q k) 1)) Filter.atTop (nhds ((excLaw θ).map Prod.snd))

The exact-size contour in the paper clock converges to the excursion height.