Bounds for the offspring defect near zero

Sequential regular variation gives a right-hand filter limit. A fixed doubling estimate then gives a lower Potter bound, by iteration on dyadic scales.

theorem BGW.StableTrees.Survival.tendsto_offspringDefect_ratio_nhdsGT {μ : PMF ℕ} {θ : ℝ} {B : ℕ → ℝ} (h : StableDomain μ θ B) {c : ℝ} (hc : 0 < c) : Filter.Tendsto (fun (u : ℝ) => offspringDefect μ (c * u) / offspringDefect μ u) (nhdsWithin 0 (Set.Ioi 0)) (nhds (c ^ θ))

Regular variation of the offspring defect as a right-hand filter limit at zero.

theorem BGW.StableTrees.Survival.exists_offspringDefect_doubling {μ : PMF ℕ} {θ : ℝ} {B : ℕ → ℝ} (h : StableDomain μ θ B) {p : ℝ} (hp : p < θ) : ∃ (v₀ : ℝ), 0 < v₀ ∧ v₀ ≤ 1 / 2 ∧ ∀ (v : ℝ), 0 < v → v ≤ v₀ → 2 ^ p * offspringDefect μ v ≤ offspringDefect μ (2 * v)

A uniform doubling lower bound with any exponent strictly below the stable index.

theorem BGW.StableTrees.Survival.offspringDefect_dyadic_lower {μ : PMF ℕ} {p v₀ : ℝ} (hd : ∀ (v : ℝ), 0 < v → v ≤ v₀ → 2 ^ p * offspringDefect μ v ≤ offspringDefect μ (2 * v)) {u : ℝ} (hu : 0 < u) (j : ℕ) (hj : 2 ^ j * u ≤ v₀) : (2 ^ p) ^ j * offspringDefect μ u ≤ offspringDefect μ (2 ^ j * u)

Iteration of a doubling lower bound, up to a fixed small scale.

theorem BGW.StableTrees.Survival.exists_offspringDefect_potter_lower {μ : PMF ℕ} {θ : ℝ} {B : ℕ → ℝ} (h : StableDomain μ θ B) {p : ℝ} (hp0 : 0 ≤ p) (hp : p < θ) : ∃ (v₀ : ℝ), 0 < v₀ ∧ v₀ ≤ 1 ∧ ∀ (u lam : ℝ), 0 < u → 1 ≤ lam → lam * u ≤ v₀ → (lam / 2) ^ p * offspringDefect μ u ≤ offspringDefect μ (lam * u)

A lower Potter bound for all multipliers at least one, below a fixed small scale.