Akra-Bazzi theorem: the sum transform

We develop further required preliminaries for the theorem, up to the sum transform.

Main definitions and results

• AkraBazziRecurrence T g a b r: the predicate stating that T : ℕ → ℝ satisfies an Akra-Bazzi recurrence with parameters g, a, b and r as above.
• GrowsPolynomially: The growth condition that g must satisfy for the theorem to apply. It roughly states that c₁ g(n) ≤ g(u) ≤ c₂ g(n), for u between b*n and n for any constant b ∈ (0,1).
• sumTransform: The transformation which turns a function g into n^p * ∑ u ∈ Finset.Ico n₀ n, g u / u^(p+1).

References

• Mohamad Akra and Louay Bazzi, On the solution of linear recurrence equations
• Tom Leighton, Notes on better master theorems for divide-and-conquer recurrences
• Manuel Eberl, Asymptotic reasoning in a proof assistant

Definition of Akra-Bazzi recurrences

This section defines the predicate AkraBazziRecurrence T g a b r which states that T satisfies the recurrence T(n) = ∑_{i=0}^{k-1} a_i T(r_i(n)) + g(n) with appropriate conditions on the various parameters.

structure AkraBazziRecurrence {α : Type u_1} [Fintype α] [Nonempty α] (T : ℕ → ℝ) (g : ℝ → ℝ) (a b : α → ℝ) (r : α → ℕ → ℕ) : Type

An Akra-Bazzi recurrence is a function that satisfies the recurrence T n = (∑ i, a i * T (r i n)) + g n.

• n₀ : ℕ

  Point below which the recurrence is in the base case

• n₀_gt_zero : 0 < self.n₀

  n₀ is always > 0

• a_pos (i : α) : 0 < a i

  The a's are nonzero

• b_pos (i : α) : 0 < b i

  The b's are nonzero

• b_lt_one (i : α) : b i < 1

  The b's are less than 1

• g_nonneg (x : ℝ) : x ≥ 0 → 0 ≤ g x

  g is nonnegative

• g_grows_poly : GrowsPolynomially g

  g grows polynomially

• h_rec (n : ℕ) (hn₀ : self.n₀ ≤ n) : T n = ∑ i : α, a i * T (r i n) + g ↑n

  The actual recurrence

• T_gt_zero' (n : ℕ) (hn : n < self.n₀) : 0 < T n

  Base case: T(n) > 0 whenever n < n₀

• r_lt_n (i : α) (n : ℕ) : self.n₀ ≤ n → r i n < n

  The r's always reduce n

• dist_r_b (i : α) : (fun (n : ℕ) => ↑(r i n) - b i * ↑n) =o[Filter.atTop] fun (n : ℕ) => ↑n / Real.log ↑n ^ 2

  The r's approximate the b's

noncomputable def AkraBazziRecurrence.min_bi {α : Type u_1} [Finite α] [Nonempty α] (b : α → ℝ) : α

Smallest b i

noncomputable def AkraBazziRecurrence.max_bi {α : Type u_1} [Finite α] [Nonempty α] (b : α → ℝ) : α

Largest b i

theorem AkraBazziRecurrence.min_bi_le {α : Type u_1} [Finite α] [Nonempty α] {b : α → ℝ} (i : α) : b (min_bi b) ≤ b i

theorem AkraBazziRecurrence.max_bi_le {α : Type u_1} [Finite α] [Nonempty α] {b : α → ℝ} (i : α) : b i ≤ b (max_bi b)

theorem AkraBazziRecurrence.isLittleO_self_div_log_id : (fun (n : ℕ) => ↑n / Real.log ↑n ^ 2) =o[Filter.atTop] fun (n : ℕ) => ↑n

theorem AkraBazziRecurrence.dist_r_b' {α : Type u_1} [Fintype α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ} [Nonempty α] (R : AkraBazziRecurrence T g a b r) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (i : α), ‖↑(r i n) - b i * ↑n‖ ≤ ↑n / Real.log ↑n ^ 2

theorem AkraBazziRecurrence.eventually_b_le_r {α : Type u_1} [Fintype α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ} [Nonempty α] (R : AkraBazziRecurrence T g a b r) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (i : α), b i * ↑n - ↑n / Real.log ↑n ^ 2 ≤ ↑(r i n)

theorem AkraBazziRecurrence.eventually_r_le_b {α : Type u_1} [Fintype α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ} [Nonempty α] (R : AkraBazziRecurrence T g a b r) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (i : α), ↑(r i n) ≤ b i * ↑n + ↑n / Real.log ↑n ^ 2

theorem AkraBazziRecurrence.eventually_r_lt_n {α : Type u_1} [Fintype α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ} [Nonempty α] (R : AkraBazziRecurrence T g a b r) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (i : α), r i n < n

theorem AkraBazziRecurrence.eventually_bi_mul_le_r {α : Type u_1} [Fintype α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ} [Nonempty α] (R : AkraBazziRecurrence T g a b r) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (i : α), b (min_bi b) / 2 * ↑n ≤ ↑(r i n)

theorem AkraBazziRecurrence.bi_min_div_two_lt_one {α : Type u_1} [Fintype α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ} [Nonempty α] (R : AkraBazziRecurrence T g a b r) : b (min_bi b) / 2 < 1

theorem AkraBazziRecurrence.bi_min_div_two_pos {α : Type u_1} [Fintype α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ} [Nonempty α] (R : AkraBazziRecurrence T g a b r) : 0 < b (min_bi b) / 2

theorem AkraBazziRecurrence.exists_eventually_const_mul_le_r {α : Type u_1} [Fintype α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ} [Nonempty α] (R : AkraBazziRecurrence T g a b r) : ∃ c ∈ Set.Ioo 0 1, ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (i : α), c * ↑n ≤ ↑(r i n)

theorem AkraBazziRecurrence.eventually_r_ge {α : Type u_1} [Fintype α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ} [Nonempty α] (R : AkraBazziRecurrence T g a b r) (C : ℝ) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (i : α), C ≤ ↑(r i n)

theorem AkraBazziRecurrence.tendsto_atTop_r {α : Type u_1} [Fintype α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ} [Nonempty α] (R : AkraBazziRecurrence T g a b r) (i : α) : Filter.Tendsto (r i) Filter.atTop Filter.atTop

theorem AkraBazziRecurrence.tendsto_atTop_r_real {α : Type u_1} [Fintype α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ} [Nonempty α] (R : AkraBazziRecurrence T g a b r) (i : α) : Filter.Tendsto (fun (n : ℕ) => ↑(r i n)) Filter.atTop Filter.atTop

theorem AkraBazziRecurrence.exists_eventually_r_le_const_mul {α : Type u_1} [Fintype α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ} [Nonempty α] (R : AkraBazziRecurrence T g a b r) : ∃ c ∈ Set.Ioo 0 1, ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (i : α), ↑(r i n) ≤ c * ↑n

theorem AkraBazziRecurrence.eventually_r_pos {α : Type u_1} [Fintype α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ} [Nonempty α] (R : AkraBazziRecurrence T g a b r) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (i : α), 0 < r i n

theorem AkraBazziRecurrence.eventually_log_b_mul_pos {α : Type u_1} [Fintype α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ} [Nonempty α] (R : AkraBazziRecurrence T g a b r) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (i : α), 0 < Real.log (b i * ↑n)

theorem AkraBazziRecurrence.T_pos {α : Type u_1} [Fintype α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ} [Nonempty α] (R : AkraBazziRecurrence T g a b r) (n : ℕ) : 0 < T n

theorem AkraBazziRecurrence.T_nonneg {α : Type u_1} [Fintype α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ} [Nonempty α] (R : AkraBazziRecurrence T g a b r) (n : ℕ) : 0 ≤ T n

Smoothing function

We define ε as the "smoothing function" fun n => 1 / log n, which will be used in the form of a factor of 1 ± ε n needed to make the induction step go through.

This is its own definition to make it easier to switch to a different smoothing function. For example, choosing 1 / log n ^ δ for a suitable choice of δ leads to a slightly tighter theorem at the price of a more complicated proof.

This part of the file then proves several properties of this function that will be needed later in the proof.

noncomputable def AkraBazziRecurrence.smoothingFn (n : ℝ) : ℝ

The "smoothing function" is defined as 1 / log n. This is defined as an ℝ → ℝ function as opposed to ℕ → ℝ since this is more convenient for the proof, where we need to e.g. take derivatives.

theorem AkraBazziRecurrence.one_add_smoothingFn_le_two {x : ℝ} (hx : Real.exp 1 ≤ x) : 1 + smoothingFn x ≤ 2

theorem AkraBazziRecurrence.isLittleO_smoothingFn_one : smoothingFn =o[Filter.atTop] fun (x : ℝ) => 1

theorem AkraBazziRecurrence.isEquivalent_one_add_smoothingFn_one : Asymptotics.IsEquivalent Filter.atTop (fun (x : ℝ) => 1 + smoothingFn x) fun (x : ℝ) => 1

theorem AkraBazziRecurrence.isEquivalent_one_sub_smoothingFn_one : Asymptotics.IsEquivalent Filter.atTop (fun (x : ℝ) => 1 - smoothingFn x) fun (x : ℝ) => 1

theorem AkraBazziRecurrence.growsPolynomially_one_sub_smoothingFn : GrowsPolynomially fun (x : ℝ) => 1 - smoothingFn x

theorem AkraBazziRecurrence.growsPolynomially_one_add_smoothingFn : GrowsPolynomially fun (x : ℝ) => 1 + smoothingFn x

theorem AkraBazziRecurrence.eventually_one_sub_smoothingFn_gt_const_real (c : ℝ) (hc : c < 1) : ∀ᶠ (x : ℝ) in Filter.atTop, c < 1 - smoothingFn x

theorem AkraBazziRecurrence.eventually_one_sub_smoothingFn_gt_const (c : ℝ) (hc : c < 1) : ∀ᶠ (n : ℕ) in Filter.atTop, c < 1 - smoothingFn ↑n

theorem AkraBazziRecurrence.eventually_one_sub_smoothingFn_pos_real : ∀ᶠ (x : ℝ) in Filter.atTop, 0 < 1 - smoothingFn x

theorem AkraBazziRecurrence.eventually_one_sub_smoothingFn_pos : ∀ᶠ (n : ℕ) in Filter.atTop, 0 < 1 - smoothingFn ↑n

theorem AkraBazziRecurrence.eventually_one_sub_smoothingFn_nonneg : ∀ᶠ (n : ℕ) in Filter.atTop, 0 ≤ 1 - smoothingFn ↑n

theorem AkraBazziRecurrence.eventually_one_sub_smoothingFn_r_pos {α : Type u_1} [Fintype α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ} [Nonempty α] (R : AkraBazziRecurrence T g a b r) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (i : α), 0 < 1 - smoothingFn ↑(r i n)

theorem AkraBazziRecurrence.differentiableAt_smoothingFn {x : ℝ} (hx : 1 < x) : DifferentiableAt ℝ smoothingFn x

theorem AkraBazziRecurrence.differentiableAt_one_sub_smoothingFn {x : ℝ} (hx : 1 < x) : DifferentiableAt ℝ (fun (z : ℝ) => 1 - smoothingFn z) x

theorem AkraBazziRecurrence.differentiableOn_one_sub_smoothingFn : DifferentiableOn ℝ (fun (z : ℝ) => 1 - smoothingFn z) (Set.Ioi 1)

theorem AkraBazziRecurrence.differentiableAt_one_add_smoothingFn {x : ℝ} (hx : 1 < x) : DifferentiableAt ℝ (fun (z : ℝ) => 1 + smoothingFn z) x

theorem AkraBazziRecurrence.differentiableOn_one_add_smoothingFn : DifferentiableOn ℝ (fun (z : ℝ) => 1 + smoothingFn z) (Set.Ioi 1)

theorem AkraBazziRecurrence.deriv_smoothingFn {x : ℝ} (hx : 1 < x) : deriv smoothingFn x = -x⁻¹ / Real.log x ^ 2

theorem AkraBazziRecurrence.isLittleO_deriv_smoothingFn : deriv smoothingFn =o[Filter.atTop] fun (x : ℝ) => x⁻¹

theorem AkraBazziRecurrence.eventually_deriv_one_sub_smoothingFn : (deriv fun (x : ℝ) => 1 - smoothingFn x) =ᶠ[Filter.atTop] fun (x : ℝ) => x⁻¹ / Real.log x ^ 2

theorem AkraBazziRecurrence.eventually_deriv_one_add_smoothingFn : (deriv fun (x : ℝ) => 1 + smoothingFn x) =ᶠ[Filter.atTop] fun (x : ℝ) => -x⁻¹ / Real.log x ^ 2

theorem AkraBazziRecurrence.isLittleO_deriv_one_sub_smoothingFn : (deriv fun (x : ℝ) => 1 - smoothingFn x) =o[Filter.atTop] fun (x : ℝ) => x⁻¹

theorem AkraBazziRecurrence.isLittleO_deriv_one_add_smoothingFn : (deriv fun (x : ℝ) => 1 + smoothingFn x) =o[Filter.atTop] fun (x : ℝ) => x⁻¹

theorem AkraBazziRecurrence.eventually_one_add_smoothingFn_pos : ∀ᶠ (n : ℕ) in Filter.atTop, 0 < 1 + smoothingFn ↑n

theorem AkraBazziRecurrence.eventually_one_add_smoothingFn_r_pos {α : Type u_1} [Fintype α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ} [Nonempty α] (R : AkraBazziRecurrence T g a b r) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (i : α), 0 < 1 + smoothingFn ↑(r i n)

theorem AkraBazziRecurrence.eventually_one_add_smoothingFn_nonneg : ∀ᶠ (n : ℕ) in Filter.atTop, 0 ≤ 1 + smoothingFn ↑n

theorem AkraBazziRecurrence.strictAntiOn_smoothingFn : StrictAntiOn smoothingFn (Set.Ioi 1)

theorem AkraBazziRecurrence.strictMonoOn_one_sub_smoothingFn : StrictMonoOn (fun (x : ℝ) => 1 - smoothingFn x) (Set.Ioi 1)

theorem AkraBazziRecurrence.strictAntiOn_one_add_smoothingFn : StrictAntiOn (fun (x : ℝ) => 1 + smoothingFn x) (Set.Ioi 1)

theorem AkraBazziRecurrence.isEquivalent_smoothingFn_sub_self {α : Type u_1} [Fintype α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ} [Nonempty α] (R : AkraBazziRecurrence T g a b r) (i : α) : Asymptotics.IsEquivalent Filter.atTop (fun (n : ℕ) => smoothingFn (b i * ↑n) - smoothingFn ↑n) fun (n : ℕ) => -Real.log (b i) / Real.log ↑n ^ 2

theorem AkraBazziRecurrence.isTheta_smoothingFn_sub_self {α : Type u_1} [Fintype α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ} [Nonempty α] (R : AkraBazziRecurrence T g a b r) (i : α) : (fun (n : ℕ) => smoothingFn (b i * ↑n) - smoothingFn ↑n) =Θ[Filter.atTop] fun (n : ℕ) => 1 / Real.log ↑n ^ 2

Akra-Bazzi exponent p

Every Akra-Bazzi recurrence has an associated exponent, denoted by p : ℝ, such that ∑ a_i b_i^p = 1. This section shows the existence and uniqueness of this exponent p for any R : AkraBazziRecurrence, and defines R.asympBound to be the asymptotic bound satisfied by R, namely n^p (1 + ∑_{u < n} g(u) / u^(p+1)).

theorem AkraBazziRecurrence.continuous_sumCoeffsExp {α : Type u_1} [Fintype α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ} [Nonempty α] (R : AkraBazziRecurrence T g a b r) : Continuous fun (p : ℝ) => ∑ i : α, a i * b i ^ p

theorem AkraBazziRecurrence.strictAnti_sumCoeffsExp {α : Type u_1} [Fintype α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ} [Nonempty α] (R : AkraBazziRecurrence T g a b r) : StrictAnti fun (p : ℝ) => ∑ i : α, a i * b i ^ p

theorem AkraBazziRecurrence.tendsto_zero_sumCoeffsExp {α : Type u_1} [Fintype α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ} [Nonempty α] (R : AkraBazziRecurrence T g a b r) : Filter.Tendsto (fun (p : ℝ) => ∑ i : α, a i * b i ^ p) Filter.atTop (nhds 0)

theorem AkraBazziRecurrence.tendsto_atTop_sumCoeffsExp {α : Type u_1} [Fintype α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ} [Nonempty α] (R : AkraBazziRecurrence T g a b r) : Filter.Tendsto (fun (p : ℝ) => ∑ i : α, a i * b i ^ p) Filter.atBot Filter.atTop

theorem AkraBazziRecurrence.one_mem_range_sumCoeffsExp {α : Type u_1} [Fintype α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ} [Nonempty α] (R : AkraBazziRecurrence T g a b r) : 1 ∈ Set.range fun (p : ℝ) => ∑ i : α, a i * b i ^ p

theorem AkraBazziRecurrence.injective_sumCoeffsExp {α : Type u_1} [Fintype α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ} [Nonempty α] (R : AkraBazziRecurrence T g a b r) : Function.Injective fun (p : ℝ) => ∑ i : α, a i * b i ^ p

The function x ↦ ∑ a_i b_i^x is injective. This implies the uniqueness of p.

theorem AkraBazziRecurrence.p_def {α : Type u_2} [Fintype α] (a b : α → ℝ) : p a b = Function.invFun (fun (p : ℝ) => ∑ i : α, a i * b i ^ p) 1

@[irreducible]

noncomputable def AkraBazziRecurrence.p {α : Type u_2} [Fintype α] (a b : α → ℝ) : ℝ

The exponent p associated with a particular Akra-Bazzi recurrence.

theorem AkraBazziRecurrence.sumCoeffsExp_p_eq_one {α : Type u_1} [Fintype α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ} [Nonempty α] (R : AkraBazziRecurrence T g a b r) : ∑ i : α, a i * b i ^ p a b = 1

The sum transform

This section defines the "sum transform" of a function g as ∑ u ∈ Finset.Ico n₀ n, g u / u^(p+1), and uses it to define asympBound as the bound satisfied by an Akra-Bazzi recurrence.

Several properties of the sum transform are then proven.

noncomputable def AkraBazziRecurrence.sumTransform (p : ℝ) (g : ℝ → ℝ) (n₀ n : ℕ) : ℝ

The transformation which turns a function g into n^p * ∑ u ∈ Finset.Ico n₀ n, g u / u^(p+1).

theorem AkraBazziRecurrence.sumTransform_def {p : ℝ} {g : ℝ → ℝ} {n₀ n : ℕ} : sumTransform p g n₀ n = ↑n ^ p * ∑ u ∈ Finset.Ico n₀ n, g ↑u / ↑u ^ (p + 1)

noncomputable def AkraBazziRecurrence.asympBound {α : Type u_1} [Fintype α] (g : ℝ → ℝ) (a b : α → ℝ) (n : ℕ) : ℝ

The asymptotic bound satisfied by an Akra-Bazzi recurrence, namely n^p (1 + ∑_{u < n} g(u) / u^(p+1)).

theorem AkraBazziRecurrence.asympBound_def (g : ℝ → ℝ) {α : Type u_2} [Fintype α] (a b : α → ℝ) {n : ℕ} : asympBound g a b n = ↑n ^ p a b + sumTransform (p a b) g 0 n

theorem AkraBazziRecurrence.asympBound_def' {g : ℝ → ℝ} {α : Type u_2} [Fintype α] (a b : α → ℝ) {n : ℕ} : asympBound g a b n = ↑n ^ p a b * (1 + ∑ u ∈ Finset.range n, g ↑u / ↑u ^ (p a b + 1))

theorem AkraBazziRecurrence.asympBound_pos {α : Type u_1} [Fintype α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ} [Nonempty α] (R : AkraBazziRecurrence T g a b r) (n : ℕ) (hn : 0 < n) : 0 < asympBound g a b n

theorem AkraBazziRecurrence.eventually_asympBound_pos {α : Type u_1} [Fintype α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ} [Nonempty α] (R : AkraBazziRecurrence T g a b r) : ∀ᶠ (n : ℕ) in Filter.atTop, 0 < asympBound g a b n

theorem AkraBazziRecurrence.eventually_asympBound_r_pos {α : Type u_1} [Fintype α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ} [Nonempty α] (R : AkraBazziRecurrence T g a b r) : ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (i : α), 0 < asympBound g a b (r i n)

theorem AkraBazziRecurrence.eventually_atTop_sumTransform_le {α : Type u_1} [Fintype α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ} [Nonempty α] (R : AkraBazziRecurrence T g a b r) : ∃ c > 0, ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (i : α), sumTransform (p a b) g (r i n) n ≤ c * g ↑n

theorem AkraBazziRecurrence.eventually_atTop_sumTransform_ge {α : Type u_1} [Fintype α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ} [Nonempty α] (R : AkraBazziRecurrence T g a b r) : ∃ c > 0, ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (i : α), c * g ↑n ≤ sumTransform (p a b) g (r i n) n