Exact-size walk and height prefix convergence #
The pair is weighted on a larger horizon and then restricted at an almost surely continuous time. This supplies the joint exact-size prefix limit along every admissible size sequence.
theorem
BGW.StableTrees.ExactPair.tendsto_exactPairLaw_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 : ℕ) => exactPairLaw μ B (q k) ⋯ a) Filter.atTop (nhds ((excLaw θ).map (restrictPair ⋯)))
Joint exact-size prefixes (C29 prefix part): along every unbounded sequence of admissible
sizes, the (walk, height) pair of the exact-size tree on [0,a], 0 < a < 1, converges jointly
to the excursion/height prefix of excLaw θ.