Local regularity for the survival time change

Continuity of the generating function and the sublinear defect at zero are consequences of summability of the offspring probabilities and their critical first moment.

theorem BGW.StableTrees.Survival.continuousOn_realGF (μ : PMF ℕ) : ContinuousOn (realGF μ) (Set.Icc 0 1)

The real generating function is continuous on the unit interval.

theorem BGW.StableTrees.Survival.continuousOn_offspringDefect (μ : PMF ℕ) : ContinuousOn (offspringDefect μ) (Set.Icc 0 1)

The offspring defect is continuous on the unit interval.

theorem BGW.StableTrees.Survival.tendsto_offspringDefect_div_self {μ : PMF ℕ} (hc : IsCritical μ) : Filter.Tendsto (fun (u : ℝ) => offspringDefect μ u / u) (nhdsWithin 0 (Set.Ioi 0)) (nhds 0)

Criticality makes the offspring defect negligible compared with its argument at zero.

theorem BGW.StableTrees.Survival.survivalProb_pos {μ : PMF ℕ} (hc : IsCritical μ) (hne : μ 1 ≠ 1) (k : ℕ) : 0 < survivalProb μ k

A critical nondegenerate tree has positive survival probability at every finite depth.

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

The decrement in one generation is precisely the offspring defect.

theorem BGW.StableTrees.Survival.tendsto_survivalProb_succ_div {μ : PMF ℕ} (hc : IsCritical μ) (hne : μ 1 ≠ 1) : Filter.Tendsto (fun (k : ℕ) => survivalProb μ (k + 1) / survivalProb μ k) Filter.atTop (nhds 1)

Adjacent survival probabilities are asymptotically equivalent.

theorem BGW.StableTrees.Survival.tendsto_offspringDefect_survivalProb_succ_div {μ : PMF ℕ} {θ : ℝ} {B : ℕ → ℝ} (h : StableDomain μ θ B) : Filter.Tendsto (fun (k : ℕ) => offspringDefect μ (survivalProb μ (k + 1)) / offspringDefect μ (survivalProb μ k)) Filter.atTop (nhds 1)

The defect at consecutive survival probabilities also has ratio tending to one.