Survival of critical BGW trees in the stable domain

Asymptotics of survival at the stable height scale and their extinction consequences.

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

The floor index k_n = ⌊δ n / B_n⌋ satisfies k_n B_n / n → δ.

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

The floor form k_n = ⌊δ n / B_n⌋.

theorem BGW.StableTrees.Survival.survival_bound {μ : PMF ℕ} {θ : ℝ} {B : ℕ → ℝ} (h : StableDomain μ θ B) {δ : ℝ} (hδ : 0 < δ) : ∃ (C : ℝ), 0 < C ∧ ∀ᶠ (n : ℕ) in Filter.atTop, B n * survivalProb μ ⌊δ * ↑n / B n⌋₊ ≤ C

The blueprint's uniform bound.

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

⌊a B_n⌋ independent trees: expected number reaching height k_n tends to a v(δ).

theorem BGW.StableTrees.Survival.tendsto_extinction_pow {μ : PMF ℕ} {θ : ℝ} {B : ℕ → ℝ} (h : StableDomain μ θ B) {δ : ℝ} (hδ : 0 < δ) {k : ℕ → ℕ} (hk : Filter.Tendsto (fun (n : ℕ) => ↑(k n) * B n / ↑n) Filter.atTop (nhds δ)) {a : ℝ} (ha : 0 ≤ a) : Filter.Tendsto (fun (n : ℕ) => (1 - survivalProb μ (k n)) ^ ⌊a * B n⌋₊) Filter.atTop (nhds (Real.exp (-(a * csbpSurvival θ δ))))

Extinction condition (DLG): ⌊a B_n⌋ independent trees all die before generation k_n with probability tending to exp(-a v(δ)).

theorem BGW.StableTrees.Survival.tendsto_floor_mul_survivalProb_floor {μ : PMF ℕ} {θ : ℝ} {B : ℕ → ℝ} (h : StableDomain μ θ B) {δ : ℝ} (hδ : 0 < δ) {a : ℝ} (ha : 0 ≤ a) : Filter.Tendsto (fun (n : ℕ) => ↑⌊a * B n⌋₊ * survivalProb μ ⌊δ * ↑n / B n⌋₊) Filter.atTop (nhds (a * csbpSurvival θ δ))

Floor form of tendsto_floor_mul_survivalProb (the K11 union bound).

theorem BGW.StableTrees.Survival.tendsto_extinction_pow_floor {μ : PMF ℕ} {θ : ℝ} {B : ℕ → ℝ} (h : StableDomain μ θ B) {δ : ℝ} (hδ : 0 < δ) {a : ℝ} (ha : 0 ≤ a) : Filter.Tendsto (fun (n : ℕ) => (1 - survivalProb μ ⌊δ * ↑n / B n⌋₊) ^ ⌊a * B n⌋₊) Filter.atTop (nhds (Real.exp (-(a * csbpSurvival θ δ))))

Floor form of tendsto_extinction_pow; a = 1 is DLG's extinction condition.