Joint convergence of the forest walk, height and contour

On every compact horizon, the padded contour is a uniformly vanishing perturbation of the interpolated height. Slutsky's theorem therefore upgrades the joint walk/height limit to the joint walk/height/contour limit, with the same continuous height in the last two coordinates.

noncomputable def BGW.StableTrees.ForestTriple.forestTriplePath (B : ℕ → ℝ) (n : ℕ) (T : NNReal) (ω : ℕ → ℕ) : Skorokhod.D ↑T ℝ × C(↑(Set.Icc 0 ↑T), ℝ) × C(↑(Set.Icc 0 ↑T), ℝ)

Forest triple path on [0,T]: the walk W_{⌊nt⌋}/B_n, the interpolated height (B_n/n) H_lin(nt) and the padded contour (B_n/n) C_lin(2nt).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def BGW.StableTrees.ForestTriple.forestTripleLaw (μ : PMF ℕ) (B : ℕ → ℝ) (n : ℕ) (T : NNReal) : MeasureTheory.ProbabilityMeasure (Skorokhod.D ↑T ℝ × C(↑(Set.Icc 0 ↑T), ℝ) × C(↑(Set.Icc 0 ↑T), ℝ))

The law of the forest triple path under the iid offspring sequence.

Equations

• BGW.StableTrees.ForestTriple.forestTripleLaw μ B n T = (BGW.StableTrees.DiscreteForest.offspringSeqLaw μ).map (BGW.StableTrees.ForestTriple.forestTriplePath B n T)

noncomputable def BGW.StableTrees.ForestTriple.forestTripleLimit (θ : ℝ) (T : NNReal) : MeasureTheory.ProbabilityMeasure (Skorokhod.D ↑T ℝ × C(↑(Set.Icc 0 ↑T), ℝ) × C(↑(Set.Icc 0 ↑T), ℝ))

The C27 limit on [0,T]: the stable path restricted to [0,T] and its continuous height (H03 prefix map), the height being used for both the height and contour coordinates.

Equations

• One or more equations did not get rendered due to their size.

theorem BGW.StableTrees.ForestTriple.measurable_forestTriplePath (B : ℕ → ℝ) (n : ℕ) (T : NNReal) : Measurable (forestTriplePath B n T)

theorem BGW.StableTrees.ForestTriple.forestTripleLaw_map_pair (μ : PMF ℕ) (B : ℕ → ℝ) (n : ℕ) (T : NNReal) : MeasureTheory.Measure.map (fun (x : Skorokhod.D ↑T ℝ × C(↑(Set.Icc 0 ↑T), ℝ) × C(↑(Set.Icc 0 ↑T), ℝ)) => (x.1, x.2.1)) ↑(forestTripleLaw μ B n T) = ↑(DiscreteForest.forestPairLaw μ B n T)

The walk/height coordinates of the triple law form the sealed forest pair law.

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

The limit in the blueprint §2 form: the graph g ↦ (g, H g, H g) pushed forward by the stable process law on [0,T] (all T).

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

C27 (Duquesne-Le Gall), every positive horizon: the rescaled walk, interpolated height and padded contour of the iid BGW forest converge jointly to (X, H, H) on [0,T].