∀ {α : Type u_1} [inst : Fintype α] [inst_1 : Nonempty α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ}
  (n₀ n₀_1 : ℕ) (e_n₀ : n₀ = n₀_1) (n₀_gt_zero : 0 < n₀) (a_pos : ∀ (i : α), 0 < a i) (b_pos : ∀ (i : α), 0 < b i)
  (b_lt_one : ∀ (i : α), b i < 1) (g_nonneg : ∀ x ≥ 0, 0 ≤ g x) (g_grows_poly : AkraBazziRecurrence.GrowsPolynomially g)
  (h_rec : ∀ (n : ℕ), n₀ ≤ n → T n = ∑ i, a i * T (r i n) + g ↑n) (T_gt_zero' : ∀ n < n₀, 0 < T n)
  (r_lt_n : ∀ (i : α) (n : ℕ), n₀ ≤ n → r i n < n)
  (dist_r_b : ∀ (i : α), (fun n => ↑(r i n) - b i * ↑n) =o[Filter.atTop] fun n => ↑n / Real.log ↑n ^ 2),
  { n₀ := n₀, n₀_gt_zero := n₀_gt_zero, a_pos := a_pos, b_pos := b_pos, b_lt_one := b_lt_one, g_nonneg := g_nonneg,
      g_grows_poly := g_grows_poly, h_rec := h_rec, T_gt_zero' := T_gt_zero', r_lt_n := r_lt_n, dist_r_b := dist_r_b } =
    { n₀ := n₀_1, n₀_gt_zero := ⋯, a_pos := a_pos, b_pos := b_pos, b_lt_one := b_lt_one, g_nonneg := g_nonneg,
      g_grows_poly := g_grows_poly, h_rec := ⋯, T_gt_zero' := ⋯, r_lt_n := ⋯, dist_r_b := dist_r_b }