Weighted convergence on the walk and height pair space

The walk marginal supplies lattice support and mass-one endpoint weights. Joint tail convergence and the joint Gamma identity identify the weighted limit.

theorem BGW.StableTrees.ExactPair.tendsto_integral_mul_prefixWeightFn_tailPairLaw {μ : 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) (F : BoundedContinuousFunction (Skorokhod.D ↑a' ℝ × C(↑(Set.Icc 0 ↑a'), ℝ)) ℝ) : Filter.Tendsto (fun (k : ℕ) => ∫ (z : Skorokhod.D ↑a' ℝ × C(↑(Set.Icc 0 ↑a'), ℝ)), F z * ExactPrefix.prefixWeightFn μ B (q k) a' z.1 ∂↑(TailPair.tailPairLaw μ B (q k) a')) Filter.atTop (nhds (∫ (z : Skorokhod.D ↑a' ℝ × C(↑(Set.Icc 0 ↑a'), ℝ)), F z ∂↑((excLaw θ).map (restrictPair ⋯))))

Weighted tail convergence at horizon a' (K07's generic helper on the pair space, J01's joint Γ identity): bounded continuous tests of the tail pair on [0,a'], weighted by the sealed walk weight, converge to the tests of the excursion/height prefix on [0,a'].