Height prefix laws under exact-size conditioning

The height marginal of the sealed joint prefix theorem supplies tightness on every strictly smaller time interval.

theorem BGW.StableTrees.ExactContour.tendsto_exactHeight_prefix {μ : PMF ℕ} {θ : ℝ} {B : ℕ → ℝ} (h : StableDomain μ θ B) {q : ℕ → ℕ} (hqtop : Filter.Tendsto q Filter.atTop Filter.atTop) (hq : ∀ (k : ℕ), Admissible μ (q k)) (a : NNReal) (ha : a ∈ Set.Ioo 0 1) : Filter.Tendsto (fun (k : ℕ) => (DiscreteForest.exactTreeLaw μ (q k)).map (TailPair.treeHeightPath B (q k) a)) Filter.atTop (nhds (((excLaw θ).map (restrictPair ⋯)).map Prod.snd))

The exact-size height prefixes converge to the height marginal of the excursion prefix.

theorem BGW.StableTrees.ExactContour.isTightMeasureSet_exactHeight_prefix {μ : PMF ℕ} {θ : ℝ} {B : ℕ → ℝ} (h : StableDomain μ θ B) {q : ℕ → ℕ} (hqtop : Filter.Tendsto q Filter.atTop Filter.atTop) (hq : ∀ (k : ℕ), Admissible μ (q k)) (a : NNReal) (ha : a ∈ Set.Ioo 0 1) : MeasureTheory.IsTightMeasureSet (Set.range fun (k : ℕ) => ↑((DiscreteForest.exactTreeLaw μ (q k)).map (TailPair.treeHeightPath B (q k) a)))

The entire sequence of height prefix laws is tight on each strict prefix.