The offspring defect at zero

The function u ↦ g(1-u)-(1-u) is the decrement in the survival recursion. This module establishes its elementary positivity and monotonicity properties.

noncomputable def BGW.StableTrees.Survival.offspringDefect (μ : PMF ℕ) (u : ℝ) : ℝ

The defect of the offspring generating function at 1-u.

Equations

• BGW.StableTrees.Survival.offspringDefect μ u = BGW.StableTrees.Survival.realGF μ (1 - u) - (1 - u)

theorem BGW.StableTrees.Survival.offspringDefect_eq_tsum (μ : PMF ℕ) (hc : IsCritical μ) {u : ℝ} (hu0 : 0 ≤ u) (hu1 : u ≤ 1) : offspringDefect μ u = ∑' (k : ℕ), (μ k).toReal * ((1 - u) ^ k - 1 + ↑k * u)

Criticality expresses the defect as a sum of nonnegative Bernoulli remainders.

theorem BGW.StableTrees.Survival.offspringDefect_nonneg {μ : PMF ℕ} (hc : IsCritical μ) {u : ℝ} (_hu0 : 0 ≤ u) (hu1 : u ≤ 1) : 0 ≤ offspringDefect μ u

The offspring defect is nonnegative on [0,1].

theorem BGW.StableTrees.Survival.offspringDefect_monotoneOn {μ : PMF ℕ} (hc : IsCritical μ) : MonotoneOn (offspringDefect μ) (Set.Icc 0 1)

The offspring defect is nondecreasing on [0,1].

theorem BGW.StableTrees.Survival.offspringDefect_pos {μ : PMF ℕ} (hc : IsCritical μ) (hne : μ 1 ≠ 1) {u : ℝ} (hu0 : 0 < u) (hu1 : u ≤ 1) : 0 < offspringDefect μ u

The offspring defect is strictly positive away from zero under critical nondegeneracy.

@[simp]

theorem BGW.StableTrees.Survival.offspringDefect_zero (μ : PMF ℕ) : offspringDefect μ 0 = 0

The offspring defect vanishes at zero.

theorem BGW.StableTrees.Survival.tendsto_offspringDefect_ratio {μ : PMF ℕ} {θ : ℝ} {B : ℕ → ℝ} (h : StableDomain μ θ B) {c : ℝ} (hc : 0 < c) {u : ℕ → ℝ} (hu : ∀ᶠ (n : ℕ) in Filter.atTop, 0 < u n) (hu0 : Filter.Tendsto u Filter.atTop (nhdsWithin 0 (Set.Ioi 0))) : Filter.Tendsto (fun (n : ℕ) => offspringDefect μ (c * u n) / offspringDefect μ (u n)) Filter.atTop (nhds (c ^ θ))

The offspring defect is regularly varying at zero, along every sequence tending to zero.