Comparison of the padded and unpadded forest contours

The walk maximum bounds the number of completed trees on a fixed contour horizon. The height modulus and the sealed contour/height comparison then control the small clock shift uniformly.

theorem BGW.StableTrees.ForestContour.unpadded_contour_error_tendstoInMeasure {μ : PMF ℕ} {θ : ℝ} {B : ℕ → ℝ} (h : StableDomain μ θ B) {T : NNReal} (hT : 0 < T) : MeasureTheory.TendstoInMeasure (↑(DiscreteForest.offspringSeqLaw μ)) (fun (n : ℕ) (ω : ℕ → ℕ) => forestContourUnpaddedError B n T ω) Filter.atTop fun (x : ℕ → ℕ) => 0

Padded/unpadded comparison on every positive horizon: the two normalized contours are uniformly close in probability.