Tail-conditioned tree walk paths

Tree path carriers and their terminal-step comparison for first-long-block extraction.

1. Shared carriers (K05b owns the path carriers; K02 copies are marked)

noncomputable def BGW.StableTrees.PathTail.treeIncrements (τ : LocallyFinite.Tree) : List ℤ

The DFS increments (d_i - 1) of a finite tree (empty list for infinite trees).

Equations

• BGW.StableTrees.PathTail.treeIncrements τ = if h : BGW.LocallyFinite.FiniteVertices τ then (BGW.PlaneTree.equivFiniteVertices.symm ⟨τ, h⟩).increments else []

@[instance_reducible]

def BGW.StableTrees.PathTail.instMeasurableSpaceListInt : MeasurableSpace (List ℤ)

The discrete σ-algebra on integer words, used locally for countable sums.

Equations

• BGW.StableTrees.PathTail.instMeasurableSpaceListInt = ⊤

theorem BGW.StableTrees.PathTail.instMeasurableSingletonClassListInt_bGW : MeasurableSingletonClass (List ℤ)

noncomputable def BGW.StableTrees.PathTail.treeIncrementSeq (τ : LocallyFinite.Tree) : ℕ → ℝ

The increments of a tree as a real sequence, extended by 0 after the end of the tree.

Equations

• BGW.StableTrees.PathTail.treeIncrementSeq τ i = ↑((BGW.StableTrees.PathTail.treeIncrements τ).getD i 0)

noncomputable def BGW.StableTrees.PathTail.treePrefixPath (B : ℕ → ℝ) (n : ℕ) (T : NNReal) (τ : LocallyFinite.Tree) : Skorokhod.D ↑T ℝ

The path t ↦ W_{⌊n t⌋}/B n of a tree on [0,T], with the sample size n (not the size of the tree) as time scale.

Equations

• BGW.StableTrees.PathTail.treePrefixPath B n T τ = BGW.Skorokhod.realStepPath (↑T) n (B n) (BGW.StableTrees.PathTail.treeIncrementSeq τ)

theorem BGW.StableTrees.PathTail.measurable_treePrefixPath (B : ℕ → ℝ) (n : ℕ) (T : NNReal) : Measurable (treePrefixPath B n T)

The prefix-path map is measurable.

noncomputable def BGW.StableTrees.PathTail.tailWalkPrefixLaw (μ : PMF ℕ) (B : ℕ → ℝ) (n : ℕ) (a : NNReal) : MeasureTheory.ProbabilityMeasure (Skorokhod.D ↑a ℝ)

The tail walk law on [0,a]: the path of a BGW tree conditioned on size ≥ n.

Equations

• BGW.StableTrees.PathTail.tailWalkPrefixLaw μ B n a = (BGW.StableTrees.DiscreteForest.tailTreeLaw μ n).map (BGW.StableTrees.PathTail.treePrefixPath B n a)

noncomputable def BGW.StableTrees.PathTail.tailPrefixLimit (θ : ℝ) (a : NNReal) : MeasureTheory.ProbabilityMeasure (Skorokhod.D ↑a ℝ)

The prefix on [0,a] of the excursion under N(· | ζ > 1) (limit of the tail walk).

Equations

• BGW.StableTrees.PathTail.tailPrefixLimit θ a = (BGW.StableTrees.tailExcursionLaw θ).map (BGW.StableTrees.excursionRestrict a)

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

The tail walk law on [0,T] for all horizons.

Equations

• BGW.StableTrees.PathTail.tailWalkLaw μ B n T = (BGW.StableTrees.DiscreteForest.tailTreeLaw μ n).map (BGW.StableTrees.PathTail.treePrefixPath B n T)

theorem BGW.StableTrees.PathTail.tailWalkPrefixLaw_eq_tailWalkLaw (μ : PMF ℕ) (B : ℕ → ℝ) (n : ℕ) (a : NNReal) : tailWalkPrefixLaw μ B n a = tailWalkLaw μ B n a

The tail walk prefix law is the tail walk law (same map).

theorem BGW.StableTrees.PathTail.tailPrefixLimit_eq_tailLevyExcLaw (θ : ℝ) (a : NNReal) : tailPrefixLimit θ a = tailLevyExcLaw θ a

The tail prefix limit is the sealed tailLevyExcLaw (same map).

2. Terminal convention: closed tree increments

noncomputable def BGW.StableTrees.PathTail.closedTreeIncrementSeq (τ : LocallyFinite.Tree) : ℕ → ℝ

The tree increments with the terminal -1 step replaced by 0 (the K04 blockIncrements convention); 0 after the end of the tree.

Equations

• BGW.StableTrees.PathTail.closedTreeIncrementSeq τ i = if i + 1 < (BGW.StableTrees.PathTail.treeIncrements τ).length then BGW.StableTrees.PathTail.treeIncrementSeq τ i else 0

theorem BGW.StableTrees.PathTail.measurable_closedTreePrefixPath (B : ℕ → ℝ) (n : ℕ) (T : NNReal) : Measurable fun (τ : LocallyFinite.Tree) => Skorokhod.realStepPath (↑T) n (B n) (closedTreeIncrementSeq τ)

The closed tree-path map is measurable.