Divide-and-conquer recurrences and the Akra-Bazzi theorem

A divide-and-conquer recurrence is a function T : ℕ → ℝ that satisfies a recurrence relation of the form T(n) = ∑_{i=0}^{k-1} a_i T(r_i(n)) + g(n) for large enough n, where r_i(n) is some function where ‖r_i(n) - b_i n‖ ∈ o(n / (log n)^2) for every i, the a_i's are some positive coefficients, and the b_i's are reals ∈ (0,1). (Note that this can be improved to O(n / (log n)^(1+ε)), this is left as future work.) These recurrences arise mainly in the analysis of divide-and-conquer algorithms such as mergesort or Strassen's algorithm for matrix multiplication. This class of algorithms works by dividing an instance of the problem of size n, into k smaller instances, where the i'th instance is of size roughly b_i n, and calling itself recursively on those smaller instances. T(n) then represents the running time of the algorithm, and g(n) represents the running time required to actually divide up the instance and process the answers that come out of the recursive calls. Since virtually all such algorithms produce instances that are only approximately of size b_i n (they have to round up or down at the very least), we allow the instance sizes to be given by some function r_i(n) that approximates b_i n.

The Akra-Bazzi theorem gives the asymptotic order of such a recurrence: it states that T(n) ∈ Θ(n^p (1 + ∑_{u=0}^{n-1} g(n) / u^{p+1})), where p is the unique real number such that ∑ a_i b_i^p = 1.

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).
• asympBound: The asymptotic bound satisfied by an Akra-Bazzi recurrence, namely n^p (1 + ∑ g(u) / u^(p+1))
• isTheta_asympBound: The main result stating that T(n) ∈ Θ(n^p (1 + ∑_{u=0}^{n-1} g(n) / u^{p+1}))

Implementation

Note that the original version of the theorem has an integral rather than a sum in the above expression, and first considers the T : ℝ → ℝ case before moving on to ℕ → ℝ. We prove the above version with a sum, as it is simpler and more relevant for algorithms.

TODO

• Specialize this theorem to the very common case where the recurrence is of the form T(n) = ℓT(r_i(n)) + g(n) where g(n) ∈ Θ(n^t) for some t. (This is often called the "master theorem" in the literature.)
• Add the original version of the theorem with an integral instead of a sum.

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 ≥ 0, 0 ≤ g x

  g is nonnegative

• g_grows_poly : AkraBazziRecurrence.GrowsPolynomially g

  g grows polynomially

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

  The actual recurrence

• T_gt_zero' : ∀ 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

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

n₀ is always > 0

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

The a's are nonzero

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

The b's are nonzero

theorem AkraBazziRecurrence.b_lt_one {α : Type u_1} [Fintype α] [Nonempty α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a : α → ℝ} {b : α → ℝ} {r : α → ℕ → ℕ} (self : AkraBazziRecurrence T g a b r) (i : α) : b i < 1

The b's are less than 1

theorem AkraBazziRecurrence.g_nonneg {α : Type u_1} [Fintype α] [Nonempty α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a : α → ℝ} {b : α → ℝ} {r : α → ℕ → ℕ} (self : AkraBazziRecurrence T g a b r) (x : ℝ) : x ≥ 0 → 0 ≤ g x

g is nonnegative

theorem AkraBazziRecurrence.g_grows_poly {α : Type u_1} [Fintype α] [Nonempty α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a : α → ℝ} {b : α → ℝ} {r : α → ℕ → ℕ} (self : AkraBazziRecurrence T g a b r) : AkraBazziRecurrence.GrowsPolynomially g

g grows polynomially

theorem AkraBazziRecurrence.h_rec {α : Type u_1} [Fintype α] [Nonempty α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a : α → ℝ} {b : α → ℝ} {r : α → ℕ → ℕ} (self : AkraBazziRecurrence T g a b r) (n : ℕ) (hn₀ : self.n₀ ≤ n) : T n = ∑ i : α, a i * T (r i n) + g ↑n

The actual recurrence

theorem AkraBazziRecurrence.T_gt_zero' {α : Type u_1} [Fintype α] [Nonempty α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a : α → ℝ} {b : α → ℝ} {r : α → ℕ → ℕ} (self : AkraBazziRecurrence T g a b r) (n : ℕ) (hn : n < self.n₀) : 0 < T n

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

theorem AkraBazziRecurrence.r_lt_n {α : Type u_1} [Fintype α] [Nonempty α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a : α → ℝ} {b : α → ℝ} {r : α → ℕ → ℕ} (self : AkraBazziRecurrence T g a b r) (i : α) (n : ℕ) : self.n₀ ≤ n → r i n < n

The r's always reduce n

theorem AkraBazziRecurrence.dist_r_b {α : Type u_1} [Fintype α] [Nonempty α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a : α → ℝ} {b : α → ℝ} {r : α → ℕ → ℕ} (self : AkraBazziRecurrence T g a b r) (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

Equations

• AkraBazziRecurrence.min_bi b = Classical.choose ⋯

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

Largest b i

Equations

• AkraBazziRecurrence.max_bi b = Classical.choose ⋯

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

theorem AkraBazziRecurrence.max_bi_le {α : Type u_1} [Finite α] [Nonempty α] {b : α → ℝ} (i : α) : b i ≤ b (AkraBazziRecurrence.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 (AkraBazziRecurrence.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 (AkraBazziRecurrence.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 (AkraBazziRecurrence.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.

Equations

• AkraBazziRecurrence.smoothingFn n = 1 / Real.log n

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

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

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

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

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

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

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

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

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

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

theorem AkraBazziRecurrence.eventually_one_sub_smoothingFn_nonneg : ∀ᶠ (n : ℕ) in Filter.atTop, 0 ≤ 1 - AkraBazziRecurrence.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 - AkraBazziRecurrence.smoothingFn ↑(r i n)

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

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

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

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

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

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

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

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

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

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

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

theorem AkraBazziRecurrence.eventually_one_add_smoothingFn_pos : ∀ᶠ (n : ℕ) in Filter.atTop, 0 < 1 + AkraBazziRecurrence.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 + AkraBazziRecurrence.smoothingFn ↑(r i n)

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

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

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

theorem AkraBazziRecurrence.strictAntiOn_one_add_smoothingFn : StrictAntiOn (fun (x : ℝ) => 1 + AkraBazziRecurrence.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 : ℕ) => AkraBazziRecurrence.smoothingFn (b i * ↑n) - AkraBazziRecurrence.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 : ℕ) => AkraBazziRecurrence.smoothingFn (b i * ↑n) - AkraBazziRecurrence.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.

@[irreducible]

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

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

Equations

• @AkraBazziRecurrence.p = AkraBazziRecurrence.wrapped✝.1

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

@[simp]

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 ^ AkraBazziRecurrence.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).

Equations

• AkraBazziRecurrence.sumTransform p g n₀ n = ↑n ^ p * ∑ u ∈ Finset.Ico n₀ n, g ↑u / ↑u ^ (p + 1)

theorem AkraBazziRecurrence.sumTransform_def {p : ℝ} {g : ℝ → ℝ} {n₀ : ℕ} {n : ℕ} : AkraBazziRecurrence.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)).

Equations

• AkraBazziRecurrence.asympBound g a b n = ↑n ^ AkraBazziRecurrence.p a b + AkraBazziRecurrence.sumTransform (AkraBazziRecurrence.p a b) g 0 n

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

theorem AkraBazziRecurrence.asympBound_def' {g : ℝ → ℝ} {α : Type u_2} [Fintype α] (a : α → ℝ) (b : α → ℝ) {n : ℕ} : AkraBazziRecurrence.asympBound g a b n = ↑n ^ AkraBazziRecurrence.p a b * (1 + ∑ u ∈ Finset.range n, g ↑u / ↑u ^ (AkraBazziRecurrence.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 < AkraBazziRecurrence.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 < AkraBazziRecurrence.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 < AkraBazziRecurrence.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 : α), AkraBazziRecurrence.sumTransform (AkraBazziRecurrence.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 ≤ AkraBazziRecurrence.sumTransform (AkraBazziRecurrence.p a b) g (r i n) n

Technical lemmas

The next several lemmas are technical lemmas leading up to rpow_p_mul_one_sub_smoothingFn_le and rpow_p_mul_one_add_smoothingFn_ge, which are key steps in the main proof.

theorem AkraBazziRecurrence.eventually_deriv_rpow_p_mul_one_sub_smoothingFn (p : ℝ) : (deriv fun (z : ℝ) => z ^ p * (1 - AkraBazziRecurrence.smoothingFn z)) =ᶠ[Filter.atTop] fun (z : ℝ) => p * z ^ (p - 1) * (1 - AkraBazziRecurrence.smoothingFn z) + z ^ (p - 1) / Real.log z ^ 2

theorem AkraBazziRecurrence.eventually_deriv_rpow_p_mul_one_add_smoothingFn (p : ℝ) : (deriv fun (z : ℝ) => z ^ p * (1 + AkraBazziRecurrence.smoothingFn z)) =ᶠ[Filter.atTop] fun (z : ℝ) => p * z ^ (p - 1) * (1 + AkraBazziRecurrence.smoothingFn z) - z ^ (p - 1) / Real.log z ^ 2

theorem AkraBazziRecurrence.isEquivalent_deriv_rpow_p_mul_one_sub_smoothingFn {p : ℝ} (hp : p ≠ 0) : Asymptotics.IsEquivalent Filter.atTop (deriv fun (z : ℝ) => z ^ p * (1 - AkraBazziRecurrence.smoothingFn z)) fun (z : ℝ) => p * z ^ (p - 1)

theorem AkraBazziRecurrence.isEquivalent_deriv_rpow_p_mul_one_add_smoothingFn {p : ℝ} (hp : p ≠ 0) : Asymptotics.IsEquivalent Filter.atTop (deriv fun (z : ℝ) => z ^ p * (1 + AkraBazziRecurrence.smoothingFn z)) fun (z : ℝ) => p * z ^ (p - 1)

theorem AkraBazziRecurrence.isTheta_deriv_rpow_p_mul_one_sub_smoothingFn {p : ℝ} (hp : p ≠ 0) : (fun (x : ℝ) => ‖deriv (fun (z : ℝ) => z ^ p * (1 - AkraBazziRecurrence.smoothingFn z)) x‖) =Θ[Filter.atTop] fun (z : ℝ) => z ^ (p - 1)

theorem AkraBazziRecurrence.isTheta_deriv_rpow_p_mul_one_add_smoothingFn {p : ℝ} (hp : p ≠ 0) : (fun (x : ℝ) => ‖deriv (fun (z : ℝ) => z ^ p * (1 + AkraBazziRecurrence.smoothingFn z)) x‖) =Θ[Filter.atTop] fun (z : ℝ) => z ^ (p - 1)

theorem AkraBazziRecurrence.growsPolynomially_deriv_rpow_p_mul_one_sub_smoothingFn (p : ℝ) : AkraBazziRecurrence.GrowsPolynomially fun (x : ℝ) => ‖deriv (fun (z : ℝ) => z ^ p * (1 - AkraBazziRecurrence.smoothingFn z)) x‖

theorem AkraBazziRecurrence.growsPolynomially_deriv_rpow_p_mul_one_add_smoothingFn (p : ℝ) : AkraBazziRecurrence.GrowsPolynomially fun (x : ℝ) => ‖deriv (fun (z : ℝ) => z ^ p * (1 + AkraBazziRecurrence.smoothingFn z)) x‖

theorem AkraBazziRecurrence.isBigO_apply_r_sub_b {α : Type u_1} [Fintype α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a : α → ℝ} {b : α → ℝ} {r : α → ℕ → ℕ} [Nonempty α] (R : AkraBazziRecurrence T g a b r) (q : ℝ → ℝ) (hq_diff : DifferentiableOn ℝ q (Set.Ioi 1)) (hq_poly : AkraBazziRecurrence.GrowsPolynomially fun (x : ℝ) => ‖deriv q x‖) (i : α) : (fun (n : ℕ) => q ↑(r i n) - q (b i * ↑n)) =O[Filter.atTop] fun (n : ℕ) => deriv q ↑n * (↑(r i n) - b i * ↑n)

theorem AkraBazziRecurrence.rpow_p_mul_one_sub_smoothingFn_le {α : 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) ^ AkraBazziRecurrence.p a b * (1 - AkraBazziRecurrence.smoothingFn ↑(r i n)) ≤ b i ^ AkraBazziRecurrence.p a b * ↑n ^ AkraBazziRecurrence.p a b * (1 - AkraBazziRecurrence.smoothingFn ↑n)

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

Main proof

This final section proves the Akra-Bazzi theorem.

theorem AkraBazziRecurrence.base_nonempty {α : Type u_1} [Fintype α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a : α → ℝ} {b : α → ℝ} {r : α → ℕ → ℕ} [Nonempty α] (R : AkraBazziRecurrence T g a b r) {n : ℕ} (hn : 0 < n) : (Finset.Ico ⌊b (AkraBazziRecurrence.min_bi b) / 2 * ↑n⌋₊ n).Nonempty

theorem AkraBazziRecurrence.T_isBigO_smoothingFn_mul_asympBound {α : Type u_1} [Fintype α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a : α → ℝ} {b : α → ℝ} {r : α → ℕ → ℕ} [Nonempty α] (R : AkraBazziRecurrence T g a b r) : T =O[Filter.atTop] fun (n : ℕ) => (1 - AkraBazziRecurrence.smoothingFn ↑n) * AkraBazziRecurrence.asympBound g a b n

The main proof of the upper bound part of the Akra-Bazzi theorem. The factor 1 - ε n does not change the asymptotic order, but is needed for the induction step to go through.

theorem AkraBazziRecurrence.smoothingFn_mul_asympBound_isBigO_T {α : Type u_1} [Fintype α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a : α → ℝ} {b : α → ℝ} {r : α → ℕ → ℕ} [Nonempty α] (R : AkraBazziRecurrence T g a b r) : (fun (n : ℕ) => (1 + AkraBazziRecurrence.smoothingFn ↑n) * AkraBazziRecurrence.asympBound g a b n) =O[Filter.atTop] T

The main proof of the lower bound part of the Akra-Bazzi theorem. The factor 1 + ε n does not change the asymptotic order, but is needed for the induction step to go through.

theorem AkraBazziRecurrence.isBigO_asympBound {α : Type u_1} [Fintype α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a : α → ℝ} {b : α → ℝ} {r : α → ℕ → ℕ} [Nonempty α] (R : AkraBazziRecurrence T g a b r) : T =O[Filter.atTop] AkraBazziRecurrence.asympBound g a b

The Akra-Bazzi theorem: T ∈ O(n^p (1 + ∑_u^n g(u) / u^{p+1}))

theorem AkraBazziRecurrence.isBigO_symm_asympBound {α : Type u_1} [Fintype α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a : α → ℝ} {b : α → ℝ} {r : α → ℕ → ℕ} [Nonempty α] (R : AkraBazziRecurrence T g a b r) : AkraBazziRecurrence.asympBound g a b =O[Filter.atTop] T

The Akra-Bazzi theorem: T ∈ Ω(n^p (1 + ∑_u^n g(u) / u^{p+1}))

theorem AkraBazziRecurrence.isTheta_asympBound {α : Type u_1} [Fintype α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a : α → ℝ} {b : α → ℝ} {r : α → ℕ → ℕ} [Nonempty α] (R : AkraBazziRecurrence T g a b r) : T =Θ[Filter.atTop] AkraBazziRecurrence.asympBound g a b

The Akra-Bazzi theorem: T ∈ Θ(n^p (1 + ∑_u^n g(u) / u^{p+1}))