Basic survival facts for critical BGW trees

This module defines the survival probability and expresses it through the offspring generating function. It also records the vanishing of survival in the critical case and the growth of the stable norming sequence.

noncomputable def BGW.StableTrees.Survival.realGF (μ : PMF ℕ) (s : ℝ) : ℝ

The real offspring generating function g(s) = ∑ μ(k) s^k. It is used on [0,1], where the series converges.

Equations

• BGW.StableTrees.Survival.realGF μ s = ∑' (k : ℕ), (μ k).toReal * s ^ k

noncomputable def BGW.StableTrees.Survival.survivalProb (μ : PMF ℕ) (k : ℕ) : ℝ

Survival to generation k: the BGW tree has a vertex at depth ≥ k, i.e. generation k is nonempty. survivalProb μ 0 = 1.

Equations

• BGW.StableTrees.Survival.survivalProb μ k = (BGW.LocallyFinite.bienaymeLaw μ.toMeasure).real (BGW.LocallyFinite.extinctBy k)ᶜ

noncomputable def BGW.StableTrees.Survival.csbpSurvival (θ δ : ℝ) : ℝ

The survival function v(δ) = ((θ-1) δ)^(-1/(θ-1)) of the continuous-state branching process with branching mechanism λ^θ (solution of v' = -v^θ with v(0+) = ∞).

Equations

• BGW.StableTrees.Survival.csbpSurvival θ δ = ((θ - 1) * δ) ^ (-1 / (θ - 1))

theorem BGW.StableTrees.Survival.survivalProb_eq_one_sub_iterate (μ : PMF ℕ) (k : ℕ) : survivalProb μ k = 1 - ((offspringGF μ.toMeasure)^[k] 0).toReal

Survival in terms of the iterated generating function.

theorem BGW.StableTrees.Survival.survivalProb_zero (μ : PMF ℕ) : survivalProb μ 0 = 1

theorem BGW.StableTrees.Survival.survivalProb_succ (μ : PMF ℕ) (k : ℕ) : survivalProb μ (k + 1) = 1 - realGF μ (1 - survivalProb μ k)

The survival recursion s(k+1) = 1 - g(1 - s(k)).

theorem BGW.StableTrees.Survival.survivalProb_mem_Icc (μ : PMF ℕ) (k : ℕ) : survivalProb μ k ∈ Set.Icc 0 1

theorem BGW.StableTrees.Survival.antitone_survivalProb (μ : PMF ℕ) : Antitone (survivalProb μ)

theorem BGW.StableTrees.Survival.tendsto_survivalProb_zero {μ : PMF ℕ} (hc : IsCritical μ) (hne : μ 1 ≠ 1) : Filter.Tendsto (survivalProb μ) Filter.atTop (nhds 0)

Critical non-degenerate trees are almost surely finite.

theorem BGW.StableTrees.Survival.tendsto_B_div_n {μ : PMF ℕ} {θ : ℝ} {B : ℕ → ℝ} (h : StableDomain μ θ B) : Filter.Tendsto (fun (n : ℕ) => B n / ↑n) Filter.atTop (nhds 0)

B_n / n → 0 (regular variation of index 1/θ < 1).

theorem BGW.StableTrees.Survival.tendsto_B_atTop {μ : PMF ℕ} {θ : ℝ} {B : ℕ → ℝ} (h : StableDomain μ θ B) : Filter.Tendsto B Filter.atTop Filter.atTop

B_n → ∞.