Tail-conditioned tree pair paths and extraction estimates

The walk retains its terminal step. The continuous height is interpolated and stopped at zero at the tree size. Both coordinates always use the same tree and the sample-size clock.

Tree height and pair paths

noncomputable def BGW.StableTrees.TailPair.treeHeightLin (τ : LocallyFinite.Tree) (u : ℝ) : ℝ

Linear interpolation at real time u of the DFS heights of a locally finite tree: the PlaneTree.heightLin of the decoded finite tree (heights |v_i| for i < z, then 0), and 0 for an infinite tree.

Equations

• BGW.StableTrees.TailPair.treeHeightLin τ u = if h : BGW.LocallyFinite.FiniteVertices τ then (BGW.PlaneTree.equivFiniteVertices.symm ⟨τ, h⟩).heightLin u else 0

theorem BGW.StableTrees.TailPair.continuous_treeHeightLin (τ : LocallyFinite.Tree) : Continuous (treeHeightLin τ)

The interpolated tree height is continuous (the junk branch of treeHeightPath never occurs).

noncomputable def BGW.StableTrees.TailPair.treeHeightPath (B : ℕ → ℝ) (n : ℕ) (T : NNReal) (τ : LocallyFinite.Tree) : C(↑(Set.Icc 0 ↑T), ℝ)

Tree height path on [0,T]: t ↦ (B n / n) * treeHeightLin τ (n t), with the sample size n (not the tree size) as time scale; junk 0 if the interpolation were discontinuous (never, continuous_treeHeightLin).

Equations

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

noncomputable def BGW.StableTrees.TailPair.treePairPath (B : ℕ → ℝ) (n : ℕ) (T : NNReal) (τ : LocallyFinite.Tree) : Skorokhod.D ↑T ℝ × C(↑(Set.Icc 0 ↑T), ℝ)

Tree pair path on [0,T]: the sealed walk path W_⌊nt⌋ / B n and the height path of the same tree.

Equations

• BGW.StableTrees.TailPair.treePairPath B n T τ = (BGW.StableTrees.PathTail.treePrefixPath B n T τ, BGW.StableTrees.TailPair.treeHeightPath B n T τ)

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

The size-tail pair law on [0,T]: the (walk, height) pair of a BGW tree conditioned on size ≥ n, at scales nt, 1/B n, B n / n.

Equations

• BGW.StableTrees.TailPair.tailPairLaw μ B n T = (BGW.StableTrees.DiscreteForest.tailTreeLaw μ n).map (BGW.StableTrees.TailPair.treePairPath B n T)

noncomputable def BGW.StableTrees.TailPair.extractedHeight (h : ℝ → ℝ) (g d t : ℝ) : ℝ

The height of the block [g, d] read off a height function h: h (g + t) for t ≤ d - g, and 0 afterwards (stopped at zero).

Equations

• BGW.StableTrees.TailPair.extractedHeight h g d t = if t ≤ d - g then h (g + t) else 0

Measurability and consistency

theorem BGW.StableTrees.TailPair.measurable_treeHeightPath (B : ℕ → ℝ) (n : ℕ) (T : NNReal) : Measurable (treeHeightPath B n T)

theorem BGW.StableTrees.TailPair.measurable_treePairPath (B : ℕ → ℝ) (n : ℕ) (T : NNReal) : Measurable (treePairPath B n T)

theorem BGW.StableTrees.TailPair.treeHeightPath_toLocallyFinite (B : ℕ → ℝ) (n : ℕ) (T : NNReal) (t : PlaneTree) (x : ↑(Set.Icc 0 ↑T)) : (treeHeightPath B n T t.toLocallyFinite) x = B n / ↑n * t.heightLin (↑n * ↑x)

On a finite tree the height path is the scaled PlaneTree.heightLin (decoding inverts toLocallyFinite).

theorem BGW.StableTrees.TailPair.treeHeightPath_eq_zero (B : ℕ → ℝ) (n : ℕ) (T : NNReal) (t : PlaneTree) (x : ↑(Set.Icc 0 ↑T)) (hx : ↑t.size ≤ ↑n * ↑x) : (treeHeightPath B n T t.toLocallyFinite) x = 0

The height path vanishes from time z/n on, z the size of the tree (stopped at zero).

theorem BGW.StableTrees.TailPair.tailPairLaw_map_fst (μ : PMF ℕ) (B : ℕ → ℝ) (n : ℕ) (T : NNReal) : (tailPairLaw μ B n T).map Prod.fst = PathTail.tailWalkLaw μ B n T

The first marginal of the pair law is exactly the sealed tail walk law.

theorem BGW.StableTrees.TailPair.map_offspringSeqLaw_firstLongTree {μ : PMF ℕ} {θ : ℝ} {B : ℕ → ℝ} (h : StableDomain μ θ B) (n : ℕ) (T : NNReal) : ((DiscreteForest.offspringSeqLaw μ).map fun (ω : ℕ → ℕ) => treePairPath B n T (DiscreteForest.firstLongTree n ω)) = tailPairLaw μ B n T

Selected discrete tree (firstLongTree_law): the pair law is the image of the iid offspring sequence under the pair path of its first ladder block of size ≥ n.

theorem BGW.StableTrees.TailPair.map_firstLongMark_excursionPair {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (T : NNReal) : ((stableLocalLaw θ).map fun (f : Skorokhod.DLoc) => excursionPair θ T (firstLongMark f)) = tailExcLaw θ T

Selected limit mark (map_firstLongMark): the target is the image of the stable law under the excursion/height pair of its first excursion longer than 1.

Locality on both sides and the finite-window coupling bound

theorem BGW.StableTrees.TailPair.treeHeightPath_blockLF (B : ℕ → ℝ) {n : ℕ} (hn : 0 < n) (T : NNReal) {ω : ℕ → ℕ} (hω : DiscreteForest.LadderFinite ω) (r : ℕ) (x : ↑(Set.Icc 0 ↑T)) : (treeHeightPath B n T (DiscreteForest.blockLF ω r)) x = extractedHeight (fun (s : ℝ) => B n / ↑n * DiscreteForest.forestHeightLin ω (↑n * s)) (↑(DiscreteForest.ladderTime ω r) / ↑n) (↑(DiscreteForest.ladderTime ω (r + 1)) / ↑n) ↑x

Discrete locality (deterministic, from forestHeight_eq_treeHeight): the height path of the r-th ladder block is the normalized forest height extracted at the block endpoints (L_r / n, L_{r+1} / n).

theorem BGW.StableTrees.TailPair.ae_excursionHeight_firstLongMark {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) : ∀ᵐ (f : Skorokhod.DLoc) ∂↑(stableLocalLaw θ), ∀ (t : NNReal), (excursionHeight θ (firstLongMark f)) t = extractedHeight (fun (s : ℝ) => heightLoc θ f s.toNNReal) (firstLongEnds f).1 (firstLongEnds f).2 ↑t

Continuous locality (height locality at the first long label): almost surely the height of the first excursion longer than 1 is the continuous host height extracted at its endpoints.

theorem BGW.StableTrees.TailPair.abs_extractedHeight_sub_le {Hn H : ℝ → ℝ} {gn dn g d M ε η t : ℝ} (hg : 0 ≤ g) (hgd : g ≤ d) (hdM : d ≤ M) (hgn : 0 ≤ gn) (hdnM : dn ≤ M) (hε : ∀ s ∈ Set.Icc 0 M, |Hn s - H s| ≤ ε) (hd : H d = 0) (hη : ∀ x ∈ Set.Icc 0 M, ∀ y ∈ Set.Icc 0 M, |x - y| ≤ |gn - g| + |dn - d| → |H x - H y| ≤ η) (ht : 0 ≤ t) : |extractedHeight Hn gn dn t - extractedHeight H g d t| ≤ ε + η

Finite-window coupling bound (deterministic): the extracted-height error is at most the uniform error ε on [0,M] plus the oscillation η of the limit height at lag |g_n - g| + |d_n - d|, given the limit endpoint zero H d = 0.