Tail-conditioned tree walk paths

The joint endpoints and cut of the first long block converge by a full-sequence Skorokhod representation localized at a deterministic source horizon. K02 coding and the uniform closing comparison identify the tail-conditioned tree-path limit on every positive horizon.

theorem BGW.StableTrees.PathTail.treePrefixPath_close_error (B : ℕ → ℝ) (n : ℕ) (T : NNReal) (τ : LocallyFinite.Tree) (t : ↑(Set.Icc 0 ↑T)) : |(treePrefixPath B n T τ) t - (Skorokhod.realStepPath (↑T) n (B n) (closedTreeIncrementSeq τ)) t| ≤ |1 / B n|

Uniform closing error between the tree path and the closed path (transfers to J1 with the identity time change).

theorem BGW.StableTrees.PathTail.dist_treePrefixPath_closed_le (B : ℕ → ℝ) (n : ℕ) (T : NNReal) (τ : LocallyFinite.Tree) : dist (treePrefixPath B n T τ) (Skorokhod.realStepPath (↑T) n (B n) (closedTreeIncrementSeq τ)) ≤ |1 / B n|

The closing estimate also bounds the Skorokhod distance by the identity time change.

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

The law of the selected first-long-block triple (endpoints and cut) of the iid walk.

Equations

• BGW.StableTrees.PathTail.selectedBlockTripleLaw μ B n T = (BGW.Probability.RealWalk.iidLaw (BGW.StableTrees.realOffspringStepLaw μ)).map (BGW.StableTrees.extractionTriple (B n) n T)

theorem BGW.StableTrees.PathTail.aemeasurable_extractionTriple {μ : PMF ℕ} {θ : ℝ} {B : ℕ → ℝ} (h : StableDomain μ θ B) (n : ℕ) (T : NNReal) : AEMeasurable (extractionTriple (B n) n T) ↑(Probability.RealWalk.iidLaw (realOffspringStepLaw μ))

Measurability (a.e.) of the extraction triple under the iid law.

theorem BGW.StableTrees.PathTail.tendsto_selectedBlockTripleLaw {μ : PMF ℕ} {θ : ℝ} {B : ℕ → ℝ} (h : StableDomain μ θ B) (T : NNReal) (hT : 0 < T) : Filter.Tendsto (fun (n : ℕ) => selectedBlockTripleLaw μ B n T) Filter.atTop (nhds ((stableLocalLaw θ).map (longCutTriple T)))

Joint endpoint/cut convergence of the first long block (retained for K14).

theorem BGW.StableTrees.PathTail.tendsto_tailWalkLaw {μ : PMF ℕ} {θ : ℝ} {B : ℕ → ℝ} (h : StableDomain μ θ B) (T : NNReal) (hT : 0 < T) : Filter.Tendsto (fun (n : ℕ) => tailWalkLaw μ B n T) Filter.atTop (nhds (tailLevyExcLaw θ T))

Tail walk path theorem (K05b main theorem). For every T > 0 the tail-conditioned tree path on [0,T] converges weakly to the excursion under N(· | ζ > 1) restricted to [0,T].

theorem BGW.StableTrees.PathTail.tendsto_tailWalkPrefixLaw {μ : PMF ℕ} {θ : ℝ} {B : ℕ → ℝ} (h : StableDomain μ θ B) {q : ℕ → ℕ} (hqtop : Filter.Tendsto q Filter.atTop Filter.atTop) (a : NNReal) (ha : a ∈ Set.Ioo 0 1) : Filter.Tendsto (fun (k : ℕ) => tailWalkPrefixLaw μ B (q k) a) Filter.atTop (nhds (tailPrefixLimit θ a))

Form consumed by K07: along an unbounded sequence, for a ∈ (0,1). There is deliberately no admissibility hypothesis: inclusive tail conditioning is not exact-size conditioning.