Vector-path form of the joint forest convergence

The walk, interpolated height and padded contour are packaged as one càdlàg path with values in ℝ × ℝ × ℝ. The packaging map is continuous, so the joint product-space convergence of the forest triple implies convergence in law of the vector path by the continuous mapping theorem.

noncomputable def BGW.StableTrees.ForestTriple.tripleVec (T : NNReal) (x : Skorokhod.D ↑T ℝ × C(↑(Set.Icc 0 ↑T), ℝ) × C(↑(Set.Icc 0 ↑T), ℝ)) : Skorokhod.D (↑T) (ℝ × ℝ × ℝ)

A walk/height/contour triple as one path in D_T(ℝ × ℝ × ℝ).

Equations

• BGW.StableTrees.ForestTriple.tripleVec T x = BGW.Skorokhod.prodWithCont x.1 (x.2.1.prodMk x.2.2)

theorem BGW.StableTrees.ForestTriple.tripleVec_apply (T : NNReal) (x : Skorokhod.D ↑T ℝ × C(↑(Set.Icc 0 ↑T), ℝ) × C(↑(Set.Icc 0 ↑T), ℝ)) (t : ↑(Set.Icc 0 ↑T)) : (tripleVec T x) t = (x.1 t, x.2.1 t, x.2.2 t)

theorem BGW.StableTrees.ForestTriple.continuous_tripleVec (T : NNReal) : Continuous (tripleVec T)

noncomputable def BGW.StableTrees.ForestTriple.forestTripleVecLaw (μ : PMF ℕ) (B : ℕ → ℝ) (n : ℕ) (T : NNReal) : MeasureTheory.ProbabilityMeasure (Skorokhod.D (↑T) (ℝ × ℝ × ℝ))

The law of the forest triple as a path in D_T(ℝ × ℝ × ℝ): walk W_{⌊nt⌋}/B_n, height (B_n/n) H_lin(nt), padded contour (B_n/n) C_lin(2nt).

Equations

• BGW.StableTrees.ForestTriple.forestTripleVecLaw μ B n T = (BGW.StableTrees.ForestTriple.forestTripleLaw μ B n T).map (BGW.StableTrees.ForestTriple.tripleVec T)

noncomputable def BGW.StableTrees.ForestTriple.forestTripleVecLimit (θ : ℝ) (T : NNReal) : MeasureTheory.ProbabilityMeasure (Skorokhod.D (↑T) (ℝ × ℝ × ℝ))

The vector C27 limit on [0,T]: the path t ↦ (X_t, H_t, H_t).

Equations

• BGW.StableTrees.ForestTriple.forestTripleVecLimit θ T = (BGW.StableTrees.ForestTriple.forestTripleLimit θ T).map (BGW.StableTrees.ForestTriple.tripleVec T)

theorem BGW.StableTrees.ForestTriple.forestTripleVecLaw_eq_map (μ : PMF ℕ) (B : ℕ → ℝ) (n : ℕ) (T : NNReal) : ↑(forestTripleVecLaw μ B n T) = MeasureTheory.Measure.map (fun (ω : ℕ → ℕ) => tripleVec T (forestTriplePath B n T ω)) ↑(DiscreteForest.offspringSeqLaw μ)

The vector law is the image of the offspring sequence law by the vector forest path.

theorem BGW.StableTrees.ForestTriple.forestTripleVecLimit_eq {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (T : NNReal) : ↑(forestTripleVecLimit θ T) = MeasureTheory.Measure.map (fun (g : Skorokhod.D ↑T ℝ) => tripleVec T (g, heightPrefix θ T g, heightPrefix θ T g)) ↑(stableProcessLaw θ ↑T)

The vector limit is the image of the stable process law on [0,T] by g ↦ (g_t, H_t, H_t)_t.

theorem BGW.StableTrees.ForestTriple.tendsto_forestTripleVecLaw {μ : PMF ℕ} {θ : ℝ} {B : ℕ → ℝ} (h : StableDomain μ θ B) {T : NNReal} (hT : 0 < T) : Filter.Tendsto (fun (n : ℕ) => forestTripleVecLaw μ B n T) Filter.atTop (nhds (forestTripleVecLimit θ T))

C27, vector-path form (Duquesne-Le Gall, Corollary 2.5.1), every positive horizon: the rescaled walk, interpolated height and padded contour of the iid BGW forest, as one path in D_T(ℝ × ℝ × ℝ), converge in law to (X, H, H) on [0,T].