Elementary consequences of the scaled survival limit

The lemmas in this file isolate the real-analytic part of the floor and extinction-step corollaries, independently of the recursion argument used to establish the scaled survival limit itself.

theorem BGW.StableTrees.Survival.exists_pos_eventually_le_of_tendsto {F : ℕ → ℝ} {v : ℝ} (hF : Filter.Tendsto F Filter.atTop (nhds v)) : ∃ (C : ℝ), 0 < C ∧ ∀ᶠ (n : ℕ) in Filter.atTop, F n ≤ C

Convergence implies an eventual upper bound with an arbitrary sign for the limit.

theorem BGW.StableTrees.Survival.tendsto_floor_mul_of_scaled {B s : ℕ → ℝ} {v a : ℝ} (hB : Filter.Tendsto B Filter.atTop Filter.atTop) (hs : Filter.Tendsto (fun (n : ℕ) => B n * s n) Filter.atTop (nhds v)) (ha : 0 ≤ a) : Filter.Tendsto (fun (n : ℕ) => ↑⌊a * B n⌋₊ * s n) Filter.atTop (nhds (a * v))

The elementary floor multiplier attached to a scaled survival limit.

theorem BGW.StableTrees.Survival.tendsto_extinction_pow_of_scaled {B s : ℕ → ℝ} {v a : ℝ} (hB : Filter.Tendsto B Filter.atTop Filter.atTop) (hs : Filter.Tendsto (fun (n : ℕ) => B n * s n) Filter.atTop (nhds v)) (hv : 0 < v) (ha : 0 ≤ a) : Filter.Tendsto (fun (n : ℕ) => (1 - s n) ^ ⌊a * B n⌋₊) Filter.atTop (nhds (Real.exp (-(a * v))))

The exponential extinction limit attached to a scaled survival limit.