Joint convergence of the forest walk and height

The walk marginal has the sealed CT5 step-path laws and the height marginal has the tight laws obtained by Arzelà-Ascoli, so the joint path laws are tight. Finite height observations retain the whole walk and are continuous. The interpolated K09 limits and the H03 graph identities identify every finite observation law, hence every subsequential limit. Prokhorov and uniqueness of the limit give convergence of the whole sequence.

theorem BGW.StableTrees.HeightTightness.isTightMeasureSet_forestPairLaw {μ : PMF ℕ} {θ : ℝ} {B : ℕ → ℝ} (h : StableDomain μ θ B) {T : NNReal} (hT : 0 < T) : MeasureTheory.IsTightMeasureSet (Set.range fun (n : ℕ) => ↑((DiscreteForest.offspringSeqLaw μ).map (DiscreteForest.forestPairPath B n T)))

Product tightness of the whole walk and interpolated forest-height paths.

theorem BGW.StableTrees.HeightTightness.map_forestPair_heightPairEval (μ : PMF ℕ) (B : ℕ → ℝ) (n : ℕ) (T : NNReal) {r : ℕ} (t : Fin r → ↑(Set.Icc 0 ↑T)) : ((DiscreteForest.offspringSeqLaw μ).map (DiscreteForest.forestPairPath B n T)).map (heightPairEval T t) = (DiscreteForest.offspringSeqLaw μ).map (interpolatedHeightJoint B n T t)

Observing a forest pair gives the interpolated finite-dimensional object.

theorem BGW.StableTrees.HeightTightness.map_heightGraph_heightPairEval {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (T : NNReal) {r : ℕ} (t : Fin r → ↑(Set.Icc 0 ↑T)) : ((stableLocalLaw θ).map fun (f : Skorokhod.DLoc) => (Skorokhod.DLoc.restrict T f, heightPrefix θ T (Skorokhod.DLoc.restrict T f))).map (heightPairEval T t) = (stableLocalLaw θ).map (DiscreteHeightApprox.heightLimitJoint θ T fun (i : Fin r) => ⟨↑(t i), ⋯⟩)

The H03 graph has the finite height observations appearing in K09.

theorem BGW.StableTrees.HeightTightness.forestPair_subseq_limit_eq_graph {μ : PMF ℕ} {θ : ℝ} {B : ℕ → ℝ} (h : StableDomain μ θ B) {T : NNReal} (hT : 0 < T) {q : ℕ → ℕ} (hq : Filter.Tendsto q Filter.atTop Filter.atTop) {P : MeasureTheory.ProbabilityMeasure (Skorokhod.D ↑T ℝ × C(↑(Set.Icc 0 ↑T), ℝ))} (hP : Filter.Tendsto (fun (j : ℕ) => (DiscreteForest.offspringSeqLaw μ).map (DiscreteForest.forestPairPath B (q j) T)) Filter.atTop (nhds P)) : P = (stableLocalLaw θ).map fun (f : Skorokhod.DLoc) => (Skorokhod.DLoc.restrict T f, heightPrefix θ T (Skorokhod.DLoc.restrict T f))

Every subsequential joint limit is the H03 walk/height graph law.

theorem BGW.StableTrees.HeightTightness.tendsto_forestPairLaw {μ : PMF ℕ} {θ : ℝ} {B : ℕ → ℝ} (h : StableDomain μ θ B) {T : NNReal} (hT : 0 < T) : Filter.Tendsto (fun (n : ℕ) => (DiscreteForest.offspringSeqLaw μ).map (DiscreteForest.forestPairPath B n T)) Filter.atTop (nhds ((stableLocalLaw θ).map fun (f : Skorokhod.DLoc) => (Skorokhod.DLoc.restrict T f, heightPrefix θ T (Skorokhod.DLoc.restrict T f))))

Joint walk/height limit on every positive horizon: the forest pair converges to the H03 graph of the stable process.