Scaling the reciprocal-defect integral

A Potter bound extended to the whole unit interval gives an integrable majorant for the rescaled reciprocal defect.

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

A lower Potter estimate valid up to the endpoint one, with a fixed positive constant.

theorem BGW.StableTrees.Survival.tendsto_survivalTime_scaled {μ : PMF ℕ} {θ : ℝ} {B : ℕ → ℝ} (h : StableDomain μ θ B) {y : ℝ} (hy : 0 < y) : Filter.Tendsto (fun (n : ℕ) => B n / ↑n * survivalTime μ (y / B n)) Filter.atTop (nhds (y ^ (1 - θ) / (θ - 1)))

The reciprocal-defect integral at a fixed stable-scale point has its power-law limit.