Documentation

Mathlib.Computability.AkraBazzi.AkraBazzi

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 #

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 #

References #

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 : α) :

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 : x0, 0 g x

    g is nonnegative

  • g grows polynomially

  • h_rec : ∀ (n : ), self.n₀ nT 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₀ nr 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

Instances For
    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 00 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) :

    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₀ nr 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
    Instances For
      noncomputable def AkraBazziRecurrence.max_bi {α : Type u_1} [Finite α] [Nonempty α] (b : α) :
      α

      Largest b i

      Equations
      Instances For
        theorem AkraBazziRecurrence.min_bi_le {α : Type u_1} [Finite α] [Nonempty α] {b : α} (i : α) :
        theorem AkraBazziRecurrence.max_bi_le {α : Type u_1} [Finite α] [Nonempty α] {b : α} (i : α) :
        theorem AkraBazziRecurrence.dist_r_b' {α : Type u_1} [Fintype α] [Nonempty α] {T : } {g : } {a : α} {b : α} {r : α} (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.isLittleO_self_div_log_id :
        (fun (n : ) => n / Real.log n ^ 2) =o[Filter.atTop] fun (n : ) => n
        theorem AkraBazziRecurrence.eventually_b_le_r {α : Type u_1} [Fintype α] [Nonempty α] {T : } {g : } {a : α} {b : α} {r : α} (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 α] [Nonempty α] {T : } {g : } {a : α} {b : α} {r : α} (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 α] [Nonempty α] {T : } {g : } {a : α} {b : α} {r : α} (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 α] [Nonempty α] {T : } {g : } {a : α} {b : α} {r : α} (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 α] [Nonempty α] {T : } {g : } {a : α} {b : α} {r : α} (R : AkraBazziRecurrence T g a b r) :
        theorem AkraBazziRecurrence.bi_min_div_two_pos {α : Type u_1} [Fintype α] [Nonempty α] {T : } {g : } {a : α} {b : α} {r : α} (R : AkraBazziRecurrence T g a b r) :
        theorem AkraBazziRecurrence.exists_eventually_const_mul_le_r {α : Type u_1} [Fintype α] [Nonempty α] {T : } {g : } {a : α} {b : α} {r : α} (R : AkraBazziRecurrence T g a b r) :
        cSet.Ioo 0 1, ∀ᶠ (n : ) in Filter.atTop, ∀ (i : α), c * n (r i n)
        theorem AkraBazziRecurrence.eventually_r_ge {α : Type u_1} [Fintype α] [Nonempty α] {T : } {g : } {a : α} {b : α} {r : α} (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 α] [Nonempty α] {T : } {g : } {a : α} {b : α} {r : α} (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 α] [Nonempty α] {T : } {g : } {a : α} {b : α} {r : α} (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 α] [Nonempty α] {T : } {g : } {a : α} {b : α} {r : α} (R : AkraBazziRecurrence T g a b r) :
        cSet.Ioo 0 1, ∀ᶠ (n : ) in Filter.atTop, ∀ (i : α), (r i n) c * n
        theorem AkraBazziRecurrence.eventually_r_pos {α : Type u_1} [Fintype α] [Nonempty α] {T : } {g : } {a : α} {b : α} {r : α} (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 α] [Nonempty α] {T : } {g : } {a : α} {b : α} {r : α} (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 α] [Nonempty α] {T : } {g : } {a : α} {b : α} {r : α} (R : AkraBazziRecurrence T g a b r) (n : ) :
        0 < T n
        theorem AkraBazziRecurrence.T_nonneg {α : Type u_1} [Fintype α] [Nonempty α] {T : } {g : } {a : α} {b : α} {r : α} (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
        Instances For
          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_r_pos {α : Type u_1} [Fintype α] [Nonempty α] {T : } {g : } {a : α} {b : α} {r : α} (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_r_pos {α : Type u_1} [Fintype α] [Nonempty α] {T : } {g : } {a : α} {b : α} {r : α} (R : AkraBazziRecurrence T g a b r) :
          ∀ᶠ (n : ) in Filter.atTop, ∀ (i : α), 0 < 1 + AkraBazziRecurrence.smoothingFn (r i n)
          theorem AkraBazziRecurrence.isEquivalent_smoothingFn_sub_self {α : Type u_1} [Fintype α] [Nonempty α] {T : } {g : } {a : α} {b : α} {r : α} (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 α] [Nonempty α] {T : } {g : } {a : α} {b : α} {r : α} (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 α] [Nonempty α] {T : } {g : } {a : α} {b : α} {r : α} (R : AkraBazziRecurrence T g a b r) :
          Continuous fun (p : ) => i : α, a i * b i ^ p
          theorem AkraBazziRecurrence.strictAnti_sumCoeffsExp {α : Type u_1} [Fintype α] [Nonempty α] {T : } {g : } {a : α} {b : α} {r : α} (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 α] [Nonempty α] {T : } {g : } {a : α} {b : α} {r : α} (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 α] [Nonempty α] {T : } {g : } {a : α} {b : α} {r : α} (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 α] [Nonempty α] {T : } {g : } {a : α} {b : α} {r : α} (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 α] [Nonempty α] {T : } {g : } {a : α} {b : α} {r : α} (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
          Instances For
            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 α] [Nonempty α] {T : } {g : } {a : α} {b : α} {r : α} (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
            Instances For
              theorem AkraBazziRecurrence.sumTransform_def {p : } {g : } {n₀ : } {n : } :
              AkraBazziRecurrence.sumTransform p g n₀ n = n ^ p * uFinset.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
              Instances For
                theorem AkraBazziRecurrence.asympBound_def' {α : Type u_1} [Fintype α] {g : } {a : α} {b : α} {n : } :
                AkraBazziRecurrence.asympBound g a b n = n ^ AkraBazziRecurrence.p a b * (1 + uFinset.range n, g u / u ^ (AkraBazziRecurrence.p a b + 1))
                theorem AkraBazziRecurrence.asympBound_pos {α : Type u_1} [Fintype α] [Nonempty α] {T : } {g : } {a : α} {b : α} {r : α} (R : AkraBazziRecurrence T g a b r) (n : ) (hn : 0 < n) :
                theorem AkraBazziRecurrence.eventually_asympBound_pos {α : Type u_1} [Fintype α] [Nonempty α] {T : } {g : } {a : α} {b : α} {r : α} (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 α] [Nonempty α] {T : } {g : } {a : α} {b : α} {r : α} (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 α] [Nonempty α] {T : } {g : } {a : α} {b : α} {r : α} (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 α] [Nonempty α] {T : } {g : } {a : α} {b : α} {r : α} (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.isBigO_apply_r_sub_b {α : Type u_1} [Fintype α] [Nonempty α] {T : } {g : } {a : α} {b : α} {r : α} (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.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.rpow_p_mul_one_sub_smoothingFn_le {α : Type u_1} [Fintype α] [Nonempty α] {T : } {g : } {a : α} {b : α} {r : α} (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 α] [Nonempty α] {T : } {g : } {a : α} {b : α} {r : α} (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 α] [Nonempty α] {T : } {g : } {a : α} {b : α} {r : α} (R : AkraBazziRecurrence T g a b r) {n : } (hn : 0 < n) :
                theorem AkraBazziRecurrence.T_isBigO_smoothingFn_mul_asympBound {α : Type u_1} [Fintype α] [Nonempty α] {T : } {g : } {a : α} {b : α} {r : α} (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 α] [Nonempty α] {T : } {g : } {a : α} {b : α} {r : α} (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 α] [Nonempty α] {T : } {g : } {a : α} {b : α} {r : α} (R : AkraBazziRecurrence T g a b r) :

                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 α] [Nonempty α] {T : } {g : } {a : α} {b : α} {r : α} (R : AkraBazziRecurrence T g a b r) :

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

                theorem AkraBazziRecurrence.isTheta_asympBound {α : Type u_1} [Fintype α] [Nonempty α] {T : } {g : } {a : α} {b : α} {r : α} (R : AkraBazziRecurrence T g a b r) :

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