Size-tail convergence of the walk and height pair #

The forest pair is coupled along the full sequence and localized where the first long block ends before a deterministic horizon. Its common endpoints select both coordinates. Letting the horizon grow removes the localization. The terminal walk step is retained in the main law.

source

noncomputable def BGW.StableTrees.TailPair.closedTreePairPath (B : ℕ → ℝ) (n : ℕ) (T : NNReal) (τ : LocallyFinite.Tree) :

Skorokhod.D ↑T ℝ × C(↑(Set.Icc 0 ↑T), ℝ )

The walk closed at the tree size, together with the height of the same tree.

Equations

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

Instances For

source

theorem BGW.StableTrees.TailPair.measurable_closedTreePairPath (B : ℕ → ℝ) (n : ℕ) (T : NNReal) :

Measurable (closedTreePairPath B n T)

The closed pair path is measurable.

source

theorem BGW.StableTrees.TailPair.tendsto_tailClosedPairLaw {μ : PMF ℕ} {θ : ℝ} {B : ℕ → ℝ} (h : StableDomain μ θ B) {T : NNReal} (hT : 0 < T) :

Filter.Tendsto (fun (n : ℕ) => (DiscreteForest.tailTreeLaw μ n).map (closedTreePairPath B n T)) Filter.atTop (nhds (tailExcLaw θ T))

The size-tail pair with the walk closed at size converges on every positive horizon.

source

theorem BGW.StableTrees.TailPair.tendsto_tailPairLaw {μ : PMF ℕ} {θ : ℝ} {B : ℕ → ℝ} (h : StableDomain μ θ B) {T : NNReal} (hT : 0 < T) :

Filter.Tendsto (fun (n : ℕ) => tailPairLaw μ B n T) Filter.atTop (nhds (tailExcLaw θ T))

C28, every positive horizon: the rescaled (walk, height) pair of a BGW tree conditioned on size ≥ n converges jointly to the excursion/height pair under N(· | ζ > 1) on [0,T].