Inverting the survival time change

The limiting time change is a strictly decreasing power function. Comparison at fixed positive scaled arguments identifies the limit for every sequence of generation indices.

theorem BGW.StableTrees.Survival.csbpSurvival_pos {θ δ : ℝ} (hθ : 1 < θ) (hδ : 0 < δ) : 0 < csbpSurvival θ δ

The CSBP survival function is positive at positive times and index greater than one.

theorem BGW.StableTrees.Survival.csbpSurvival_time {θ δ : ℝ} (hθ : 1 < θ) (hδ : 0 < δ) : csbpSurvival θ δ ^ (1 - θ) / (θ - 1) = δ

Substitution of the CSBP survival function into the limiting time change.

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

A positive height-scale limit forces the generation indices to infinity.

theorem BGW.StableTrees.Survival.tendsto_survivalProb_scaled {μ : PMF ℕ} {θ : ℝ} {B : ℕ → ℝ} (h : StableDomain μ θ B) {δ : ℝ} (hδ : 0 < δ) {k : ℕ → ℕ} (hk : Filter.Tendsto (fun (n : ℕ) => ↑(k n) * B n / ↑n) Filter.atTop (nhds δ)) : Filter.Tendsto (fun (n : ℕ) => B n * survivalProb μ (k n)) Filter.atTop (nhds (csbpSurvival θ δ))

Survival at the height scale. If k_n B_n / n → δ > 0, then B_n s(k_n) → ((θ-1) δ)^(-1/(θ-1)).