Documentation

BGW.StableTrees.SurvivalIntegral

Integral time change for survival #

The integral of the reciprocal defect increases asymptotically by one along the survival recursion. Its value at the survival probability is therefore asymptotic to the generation.

source
noncomputable def BGW.StableTrees.Survival.survivalTime (μ : PMF ℕ) (x : ℝ) :
ℝ

The reciprocal-defect time change, used for arguments in (0,1].

Equations
Instances For
    source
    theorem BGW.StableTrees.Survival.intervalIntegrable_inv_offspringDefect {μ : PMF ℕ} (hc : IsCritical μ) (hne : μ 1 ≠ 1) {a b : ℝ} (ha : 0 < a) (hab : a ≤ b) (hb : b ≤ 1) :
    IntervalIntegrable (fun (u : ℝ) => (offspringDefect μ u)⁻¹) MeasureTheory.volume a b

    The reciprocal defect is integrable on every compact interval in (0,1].

    source
    theorem BGW.StableTrees.Survival.survivalTime_antitoneOn {μ : PMF ℕ} (hc : IsCritical μ) (hne : μ 1 ≠ 1) :
    AntitoneOn (survivalTime μ) (Set.Ioc 0 1)

    The time change is antitone on its positive domain.

    source
    theorem BGW.StableTrees.Survival.survivalTime_succ_bounds {μ : PMF ℕ} (hc : IsCritical μ) (hne : μ 1 ≠ 1) (k : ℕ) :
    1 ≤ survivalTime μ (survivalProb μ (k + 1)) - survivalTime μ (survivalProb μ k) ∧ survivalTime μ (survivalProb μ (k + 1)) - survivalTime μ (survivalProb μ k) ≤ offspringDefect μ (survivalProb μ k) / offspringDefect μ (survivalProb μ (k + 1))

    One survival step increases the time change by an amount between one and the defect ratio.

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

    The time-change increment tends to one along successive generations.

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

    The integral time change at generation k is asymptotic to k.