Exact-size Łukasiewicz prefixes through tail conditioning #

The finite prefix Radon–Nikodym identity and compact-uniform forest estimates transfer convergence of tail-conditioned paths to the unit excursion prefix law. Mass one and Scheffé's theorem control the weights at both ends of the positive half-line.

source

theorem BGW.StableTrees.ExactPrefix.integral_prefixWeightFn_tail {μ : PMF ℕ} {θ : ℝ} {B : ℕ → ℝ} (h : StableDomain μ θ B) {n : ℕ} (hn : Admissible μ n) (a : NNReal) (ha : a ∈ Set.Ioo 0 1) :

(∀ (x : Skorokhod.D ↑a ℝ), 0 ≤ prefixWeightFn μ B n a x) ∧ ∫ (x : Skorokhod.D ↑a ℝ), prefixWeightFn μ B n a x ∂↑(PathTail.tailWalkPrefixLaw μ B n a) = 1

The weight is nonnegative and has mean one under the tail walk prefix law (K02 lintegral_prefixDensity_tail).

source

theorem BGW.StableTrees.ExactPrefix.tendsto_exactWalkLaw_prefix {μ : PMF ℕ} {θ : ℝ} {B : ℕ → ℝ} (h : StableDomain μ θ B) {q : ℕ → ℕ} (hqtop : Filter.Tendsto q Filter.atTop Filter.atTop) (hq : ∀ (k : ℕ), Admissible μ (q k)) (a : NNReal) (ha : a ∈ Set.Ioo 0 1) :

Filter.Tendsto (fun (k : ℕ) => exactWalkPrefixLaw μ B (q k) ⋯ a ⋯) Filter.atTop (nhds ((unitExcursionLaw θ).map (excursionRestrict a)))

Exact-size walk prefixes (K07 main theorem). Along an unbounded sequence of admissible sizes the exact-size Łukasiewicz path on [0,a], a ∈ (0,1), scaled by B (q k), converges weakly to the prefix of the unit excursion law.