theorem tendsto_and_summable_of_summable_perturbed_descent {α β γ ε : ℕ → NNReal} (hγ : Summable γ) (hε : Summable ε) (hrec : ∀ (n : ℕ), α (n + 1) + β n ≤ (1 + γ n) * α n + ε n) : (∃ (l : NNReal), Filter.Tendsto α Filter.atTop (nhds l)) ∧ Summable β

Lemma 5.31: if nonnegative sequences α and β satisfy the perturbed descent recursion α (n + 1) + β n ≤ (1 + γ n) * α n + ε n and the perturbation sequences γ and ε are summable, then α converges in ℝ≥0 and β is summable.