Forest masses and prefix weights

Canonical forest mass, inclusive tail and exact-prefix weight definitions. The probability identities retain extinction and admissibility hypotheses explicitly.

Reference: J.-F. Le Gall, Random trees and applications, Probab. Surveys 2 (2005), Section 1.

def BGW.StableTrees.Admissible (μ : PMF ℕ) (n : ℕ) : Prop

Admissible size: the exact-size mass P[ζ = n] is nonzero.

Equations

• BGW.StableTrees.Admissible μ n = ((BGW.LocallyFinite.bienaymeLaw μ.toMeasure) (BGW.LocallyFinite.sizeEvent n) ≠ 0)

noncomputable def BGW.StableTrees.forestMass (μ : PMF ℕ) (j r : ℕ) : ℝ

f_j(r): probability that a j-forest of Bienaymé trees has r vertices.

Equations

• BGW.StableTrees.forestMass μ j r = (BGW.forestWeight (⇑μ) j r).toReal

noncomputable def BGW.StableTrees.forestTail (μ : PMF ℕ) (j r : ℕ) : ℝ

G_j(r) = ∑_{k ≥ r} f_j(k): probability that a j-forest has at least r vertices.

Equations

• BGW.StableTrees.forestTail μ j r = ∑' (k : ℕ), (Set.Ici r).indicator (fun (k : ℕ) => BGW.StableTrees.forestMass μ j k) k

noncomputable def BGW.StableTrees.exactPrefixWeight (μ : PMF ℕ) (n m j : ℕ) : ℝ

Discrete RN weight R_n(m,j) = f_j(n-m)/G_j(n-m) * G_1(n)/f_1(n) from the tail-conditioned law to the exact-size law, at prefix length m < n with j = W_m + 1 (totalized division).

Equations

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

theorem BGW.StableTrees.forestMass_one_eq_sizeProb (μ : PMF ℕ) (n : ℕ) : forestMass μ 1 n = (LocallyFinite.bienaymeLaw μ.toMeasure).real (LocallyFinite.sizeEvent n)

f_1(n) = P[ζ = n].

theorem BGW.StableTrees.forestTail_one_eq_sizeGe {μ : PMF ℕ} (hc : IsCritical μ) (hne : μ 1 ≠ 1) (n : ℕ) : forestTail μ 1 n = (LocallyFinite.bienaymeLaw μ.toMeasure).real (Attraction.sizeGeEvent n)

G_1(n) = P[ζ ≥ n] for a critical non-degenerate law.

theorem BGW.StableTrees.exactMass_tendsto {μ : PMF ℕ} {θ : ℝ} {B : ℕ → ℝ} (h : StableDomain μ θ B) {q : ℕ → ℕ} (hqtop : Filter.Tendsto q Filter.atTop Filter.atTop) (hq : ∀ (k : ℕ), Admissible μ (q k)) : Filter.Tendsto (fun (k : ℕ) => ↑(q k) * B (q k) * forestMass μ 1 (q k)) Filter.atTop (nhds (↑(Scalar.latticeSpan μ) * Scalar.stableDensity θ 0))

Exact mass along an explicit unbounded admissible sequence: q_k B_{q_k} f_1(q_k) → d p₁(0) (false along all integers when d > 1).