{α : Type u_1} →
  [inst : Fintype α] →
    [inst_1 : Nonempty α] →
      {T : ℕ → ℝ} →
        {g : ℝ → ℝ} →
          {a b : α → ℝ} →
            {r : α → ℕ → ℕ} →
              (n₀ : ℕ) →
                0 < n₀ →
                  (∀ (i : α), 0 < a i) →
                    (∀ (i : α), 0 < b i) →
                      (∀ (i : α), b i < 1) →
                        (∀ x ≥ 0, 0 ≤ g x) →
                          AkraBazziRecurrence.GrowsPolynomially g →
                            (∀ (n : ℕ), n₀ ≤ n → T n = ∑ i, a i * T (r i n) + g ↑n) →
                              (∀ n < n₀, 0 < T n) →
                                (∀ (i : α) (n : ℕ), n₀ ≤ n → r i n < n) →
                                  (∀ (i : α),
                                      (fun n => ↑(r i n) - b i * ↑n) =o[Filter.atTop] fun n => ↑n / Real.log ↑n ^ 2) →
                                    AkraBazziRecurrence T g a b r