AkraBazziRecurrence.g_grows_poly
theorem AkraBazziRecurrence.g_grows_poly :
∀ {α : Type u_1} [inst : Fintype α] [inst_1 : Nonempty α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ},
AkraBazziRecurrence T g a b r → AkraBazziRecurrence.GrowsPolynomially g
The theorem `AkraBazziRecurrence.g_grows_poly` asserts that for a given function `g` which is part of an Akra-Bazzi recurrence `T`, the function `g` grows polynomially. More specifically, if `T` is an Akra-Bazzi recurrence that involves the function `g`, and sequences `a`, `b`, and `r`, then `g` satisfies the growth condition defined by `AkraBazziRecurrence.GrowsPolynomially`. This growth condition essentially states that for any constant `b` between 0 and 1, there exist positive constants `c₁` and `c₂` such that the value of `g(u)` is between `c₁ * g(n)` and `c₂ * g(n)` for `u` between `b*n` and `n`. This is a condition that ensures 'polynomial' growth of function `g` in terms of `n` in the context of the Akra-Bazzi method for solving recurrences.
More concisely: For a function `g` in an Akra-Bazzi recurrence `T`, there exist constants `c₁, c₂` such that `g(u)` is bounded between `c₁ * g(n)` and `c₂ * g(n)` for `u` in the range `[b*n, n]`, where `b` is a constant between 0 and 1.
|
AkraBazziRecurrence.differentiableAt_smoothingFn
theorem AkraBazziRecurrence.differentiableAt_smoothingFn :
∀ {x : ℝ}, 1 < x → DifferentiableAt ℝ AkraBazziRecurrence.smoothingFn x
The theorem `AkraBazziRecurrence.differentiableAt_smoothingFn` states that for all real numbers `x` where `x` is greater than 1, the function `smoothingFn` from the Akra-Bazzi recurrence, defined as `1 / log(n)`, is differentiable at `x`. Differentiability means that at the point `x`, the function has a derivative, which can possibly be non-unique. In practical terms, the function smoothly changes at these points without any sharp turns or breaks.
More concisely: For `x` being a real number greater than 1, the function `1 / log(x)` from the Akra-Bazzi recurrence is differentiable at `x`.
|
AkraBazziRecurrence.T_gt_zero'
theorem AkraBazziRecurrence.T_gt_zero' :
∀ {α : Type u_1} [inst : Fintype α] [inst_1 : Nonempty α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ}
(self : AkraBazziRecurrence T g a b r), ∀ n < self.n₀, 0 < T n
This theorem, "AkraBazziRecurrence.T_gt_zero'", states that for any natural number `n` which is less than a certain threshold `n₀` in the context of the Akra-Bazzi recurrence, the value of the function `T` at `n` is always greater than zero. This is true irrespective of the type `α`, which has a finite number of instances and at least one instance, and the functions `g`, `a`, `b`, and `r` that take arguments of type `α` or natural numbers.
More concisely: For any instance `α` of a finite type with at least one element, and for all natural numbers `n` less than a certain threshold `n₀`, the value of the function `T` from the Akra-Bazzi recurrence with functions `g`, `a`, `b`, and `r` is strictly positive.
|
AkraBazziRecurrence.n₀_gt_zero
theorem AkraBazziRecurrence.n₀_gt_zero :
∀ {α : Type u_1} [inst : Fintype α] [inst_1 : Nonempty α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ}
(self : AkraBazziRecurrence T g a b r), 0 < self.n₀
The theorem `AkraBazziRecurrence.n₀_gt_zero` states that for any `AkraBazziRecurrence` instance, with `T` as a function from natural numbers to real numbers, `g` as a function from real numbers to real numbers, `a` and `b` as functions from a given finite type `α` to real numbers, and `r` as a function from `α` to a function from natural numbers to natural numbers, the value of `self.n₀` is always greater than zero. The `AkraBazziRecurrence` is a particular form of recurrent relation often used in the analysis of algorithms, and `n₀` is a parameter of this recurrence. This theorem ensures that `n₀` is strictly positive for all instances of `AkraBazziRecurrence`.
More concisely: For any `AkraBazziRecurrence` instance with real-valued functions `T`, `g`, `a`, and `r` over a finite type `α`, the initial value `n₀` is strictly positive.
|
AkraBazziRecurrence.isBigO_asympBound
theorem AkraBazziRecurrence.isBigO_asympBound :
∀ {α : Type u_1} [inst : Fintype α] [inst_1 : Nonempty α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ},
AkraBazziRecurrence T g a b r → T =O[Filter.atTop] AkraBazziRecurrence.asympBound g a b
This is the Akra-Bazzi theorem which states that for a given Akra-Bazzi recurrence `T`, function `g`, and functions `a` and `b` of a finite type `α` (which has at least one element) along with a function `r` from `α` to a function from natural numbers to natural numbers, if the recurrence `T` follows the Akra-Bazzi form with parameters `g`, `a`, `b` and `r`, then the function `T` has an asymptotic upper bound. This upper bound is given by `n^p (1 + ∑_{u < n} g(u) / u^{p+1})` where `p` is a certain constant determined by `a` and `b`. The asymptotic upper bound is expressed in terms of big O notation as `T ∈ O(n^p (1 + ∑_{u < n} g(u) / u^{p+1}))` for `n` going to infinity.
More concisely: The Akra-Bazzi theorem states that for an Akra-Bazzi recurrence `T` with parameters `g`, `a`, `b`, and `r`, if `T` follows the Akra-Bazzi form, then `T` has an asymptotic upper bound `O(n^p (1 + ∑ₙ₁^(-(p+1)) g(n)))`, where `p` is a constant determined by `a` and `b`.
|
AkraBazziRecurrence.isEquivalent_one_add_smoothingFn_one
theorem AkraBazziRecurrence.isEquivalent_one_add_smoothingFn_one :
Asymptotics.IsEquivalent Filter.atTop (fun x => 1 + AkraBazziRecurrence.smoothingFn x) fun x => 1
This theorem states that the function `1 + AkraBazziRecurrence.smoothingFn x`, where the smoothing function is defined as `1 / log x`, is asymptotically equivalent to the function `1` as `x` goes to infinity (symbolized by `Filter.atTop`). In more mathematical terms, it means that the difference between the two functions `(1 + 1 / log x) - 1` becomes infinitesimally small compared to `1` as `x` approaches infinity.
More concisely: As x approaches infinity, the difference between `1 + 1 / log x` and `1` approaches 0.
|
AkraBazziRecurrence.dist_r_b
theorem AkraBazziRecurrence.dist_r_b :
∀ {α : Type u_1} [inst : Fintype α] [inst_1 : Nonempty α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ},
AkraBazziRecurrence T g a b r →
∀ (i : α), (fun n => ↑(r i n) - b i * ↑n) =o[Filter.atTop] fun n => ↑n / (↑n).log ^ 2
This theorem is named `AkraBazziRecurrence.dist_r_b` and is related to the Akra-Bazzi method for solving recurrence relations. The theorem states that for any type `α` that is finite and nonempty, and given real-valued functions `T`, `g`, `a`, `b`, and `r` indexed by `α` and `ℕ`, if these functions satisfy the Akra-Bazzi recurrence relation, then for each value `i` of type `α`, the difference between `r i n` and `b i` times `n` is asymptotically equivalent (as `n` approaches infinity) to the function `n / log²(n)`. In mathematical terms, the function `(r i n) - b i * n` is little o of the function `n / log²(n)` as `n` goes to infinity.
More concisely: For any finite and nonempty type `α` and real-valued functions `T`, `g`, `a`, `b`, and `r` indexed by `α` and `ℕ`, if `r`, `a`, and `b` satisfy the Akra-Bazzi recurrence relation, then `r i n - b i * n = o(n / log²(n))` as `n` goes to infinity for each `i` of type `α`.
|
AkraBazziRecurrence.g_nonneg
theorem AkraBazziRecurrence.g_nonneg :
∀ {α : Type u_1} [inst : Fintype α] [inst_1 : Nonempty α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ},
AkraBazziRecurrence T g a b r → ∀ x ≥ 0, 0 ≤ g x
This theorem, named `AkraBazziRecurrence.g_nonneg`, states that for all nonnegative real numbers `x`, the function `g` is nonnegative given certain conditions. More specifically, for any type `α` with instances of `Fintype` and `Nonempty`, for any functions `T : ℕ → ℝ`, `g : ℝ → ℝ`, `a : α → ℝ`, `b : α → ℝ`, and `r : α → ℕ → ℕ`, if the Akra-Bazzi Recurrence holds for these functions, then for all `x` such that `x` is greater than or equal to 0, `g(x)` is also greater than or equal to 0.
More concisely: If `T`, `g`, `a`, `b`, and `r` satisfy the Akra-Bazzi Recurrence condition, then for all `α` in `Fintype` and `Nonempty`, and for all `x ∈ ℝ` with `x ≥ 0`, `g(x) ≥ 0`.
|
AkraBazziRecurrence.injective_sumCoeffsExp
theorem AkraBazziRecurrence.injective_sumCoeffsExp :
∀ {α : Type u_1} [inst : Fintype α] [inst_1 : Nonempty α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ},
AkraBazziRecurrence T g a b r → Function.Injective fun p => Finset.univ.sum fun i => a i * b i ^ p
The theorem `AkraBazziRecurrence.injective_sumCoeffsExp` states that for any type `α` that is a finite and nonempty set, a function `T` from natural numbers to real numbers, a function `g` from real numbers to real numbers, and functions `a`, `b`, and `r` from `α` to real numbers and natural numbers respectively that satisfy the Akra-Bazzi recurrence, the function which maps a real number `p` to the sum over all elements `i` in `α` of `a(i) * b(i)^p` is injective. In other words, if two different real numbers `p` and `q` produce the same sum, then `p` must equal `q`. This implies that `p` is unique under these conditions and can't have different values producing the same result.
More concisely: If `α` is a finite and nonempty set, `T : ℕ → ℝ`, `g : ℝ → ℝ`, and `a : α → ℝ`, `b : α → ℕ`, and `r : α → ℕ` satisfy the Akra-Bazzi recurrence, then the map `p : ℝ → ∑ i in α (a i * b i ^ p)` is injective.
|
AkraBazziRecurrence.tendsto_atTop_r
theorem AkraBazziRecurrence.tendsto_atTop_r :
∀ {α : Type u_1} [inst : Fintype α] [inst_1 : Nonempty α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ},
AkraBazziRecurrence T g a b r → ∀ (i : α), Filter.Tendsto (r i) Filter.atTop Filter.atTop
This theorem, named `AkraBazziRecurrence.tendsto_atTop_r`, states that for any type `α` that is a finite nonempty set, and functions `T : ℕ → ℝ`, `g : ℝ → ℝ`, `a : α → ℝ`, `b : α → ℝ`, and `r : α → ℕ → ℕ`, if the Akra-Bazzi Recurrence relation holds for `T`, `g`, `a`, `b`, and `r`, then for every `i` in `α`, the function `r i` tends to infinity as its argument tends to infinity. In other words, for every neighborhood of infinity in the codomain, there is a neighborhood of infinity in the domain such that the image of the latter neighborhood under `r i` is contained in the former neighborhood.
More concisely: For any finite nonempty set `α`, functions `T : ℕ → ℝ`, `g : ℝ → ℝ`, `a : α → ℝ`, `b : α → ℝ`, and `r : α → ℕ → ℕ` satisfying the Akra-Bazzi Recurrence relation, for all `i` in `α`, the sequence `r i x` goes to infinity as `x` goes to infinity.
|
AkraBazziRecurrence.b_lt_one
theorem AkraBazziRecurrence.b_lt_one :
∀ {α : Type u_1} [inst : Fintype α] [inst_1 : Nonempty α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ},
AkraBazziRecurrence T g a b r → ∀ (i : α), b i < 1
This theorem states that for any Akra-Bazzi recurrence, given by the function `T`, the parameter `b` (which is a function from some finite type `α` to the real numbers `ℝ`) is always less than 1 for all elements of `α`. Here, the Akra-Bazzi recurrence `T` is defined in terms of other functions `g`, `a`, `b`, and `r` and the functions `a`, `b`, and `r` are from the finite type `α` to the real numbers `ℝ` or natural numbers `ℕ`, respectively. This theorem holds for all types `α` where `α` is nonempty and finite.
More concisely: For any Akra-Bazzi recurrence `T` defined by functions `g`, `a`, `b` (from a nonempty, finite type `α` to `ℝ`), and `r` (from `α` to `ℕ`), the parameter `b` is strictly less than 1 for all elements of `α`.
|
AkraBazziRecurrence.r_lt_n
theorem AkraBazziRecurrence.r_lt_n :
∀ {α : Type u_1} [inst : Fintype α] [inst_1 : Nonempty α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ}
(self : AkraBazziRecurrence T g a b r) (i : α) (n : ℕ), self.n₀ ≤ n → r i n < n
This theorem, `AkraBazziRecurrence.r_lt_n`, states that for any Akra-Bazzi recurrence `T` with auxiliary function `g`, coefficients `a` and `b`, and function `r`, if `n` is greater than or equal to `n₀` (the base case for our recurrence `T`), then the function `r` when applied to `i` and `n`, is always less than `n`. This property holds for every instance `i` of a finite, non-empty type `α`. Essentially, it's saying that the `r` functions always reduce `n` in the context of this Akra-Bazzi recurrence.
More concisely: For any Akra-Bazzi recurrence `T` with auxiliary function `g`, coefficients `a` and `b`, and function `r`, if `n >= n0`, then for all `i` in the finite, non-empty type `α`, `r(i, n) < n`.
|
AkraBazziRecurrence.deriv_smoothingFn
theorem AkraBazziRecurrence.deriv_smoothingFn :
∀ {x : ℝ}, 1 < x → deriv AkraBazziRecurrence.smoothingFn x = -x⁻¹ / x.log ^ 2
The theorem `AkraBazziRecurrence.deriv_smoothingFn` states that for any real number `x` such that `x` is greater than 1, the derivative of the Akra-Bazzi recurrence's smoothing function, which is defined as `1 / log(n)`, at `x` is equal to `-1 / (x * log(x)^2)`. This theorem communicates the rate of change of the smoothing function at any point `x` greater than 1 in the context of the Akra-Bazzi recurrence.
More concisely: For `x` greater than 1, the derivative of the Akra-Bazzi recurrence's smoothing function `1 / log(n)` is equal to `-1 / (x * log(x)^2)`.
|
AkraBazziRecurrence.h_rec
theorem AkraBazziRecurrence.h_rec :
∀ {α : Type u_1} [inst : Fintype α] [inst_1 : Nonempty α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ}
(self : AkraBazziRecurrence T g a b r) (n : ℕ),
self.n₀ ≤ n → T n = (Finset.univ.sum fun i => a i * T (r i n)) + g ↑n
This theorem states that for any type `α` which is finite and nonempty, and for any functions `T : ℕ → ℝ`, `g : ℝ → ℝ`, `a : α → ℝ`, `b : α → ℝ`, and `r : α → ℕ → ℕ`, given an instance of `AkraBazziRecurrence` involving these functions, and for any natural number `n` greater than or equal to `self.n₀`, the function `T` at `n` equals the sum (taken over the universal finite set of type `α`) of the product of the function `a` at `i` and the function `T` at `r i n`, plus the function `g` at `n`, where `i` is an element of the universal finite set of type `α`. Essentially, this theorem defines the Akra-Bazzi recurrence relation.
More concisely: For any finite and nonempty type `α` and functions `T : ℕ → ℝ`, `g : ℝ → ℝ`, `a : α → ℝ`, `b : α → ℕ → ℕ`, if `T` satisfies the Akra-Bazzi recurrence relation defined by `a`, `T`, `g`, and `r`, then for all `n ≥ self.n0`, `T n = ∑i∈α (a i * T (r i n)) + g n`.
|
AkraBazziRecurrence.smoothingFn_mul_asympBound_isBigO_T
theorem AkraBazziRecurrence.smoothingFn_mul_asympBound_isBigO_T :
∀ {α : Type u_1} [inst : Fintype α] [inst_1 : Nonempty α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ},
AkraBazziRecurrence T g a b r →
(fun n => (1 + AkraBazziRecurrence.smoothingFn ↑n) * AkraBazziRecurrence.asympBound g a b n) =O[Filter.atTop]
T
This theorem represents the main proof of the lower bound part of the Akra-Bazzi theorem within the context of recurrence relations. It establishes that the function `(1 + AkraBazziRecurrence.smoothingFn n) * AkraBazziRecurrence.asympBound g a b n`, where `n` is a positive real number, `g` is a function from real numbers to real numbers, and `a` and `b` are functions from an arbitrary fintype α to real numbers, is a big-O of the function `T` as `n` approaches infinity, provided that `T` is an Akra-Bazzi recurrence dictated by `g`, `a`, `b`, and a function `r` from α to natural numbers. The factor `1 + AkraBazziRecurrence.smoothingFn n` does not alter the asymptotic order of the equation, but is necessary to facilitate the induction step of the proof.
More concisely: If `T(n)` is an Akra-Bazzi recurrence with smoothing function `AkraBazziRecurrence.smoothingFn` and asymptotic bound `g`, then `(1 + AkraBazziRecurrence.smoothingFn n) * g(n)` is a big-O estimate for `T(n)` as `n` approaches infinity.
|
AkraBazziRecurrence.T_isBigO_smoothingFn_mul_asympBound
theorem AkraBazziRecurrence.T_isBigO_smoothingFn_mul_asympBound :
∀ {α : Type u_1} [inst : Fintype α] [inst_1 : Nonempty α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ},
AkraBazziRecurrence T g a b r →
T =O[Filter.atTop] fun n => (1 - AkraBazziRecurrence.smoothingFn ↑n) * AkraBazziRecurrence.asympBound g a b n
This theorem, `AkraBazziRecurrence.T_isBigO_smoothingFn_mul_asympBound`, states that for any Akra-Bazzi recurrence `T`, defined with respect to given functions `g`, `a`, `b` and `r`, the function `T` is bounded above asymptotically (as `n` approaches infinity) by the function `(1 - AkraBazziRecurrence.smoothingFn n) * AkraBazziRecurrence.asympBound g a b n`. Here, `AkraBazziRecurrence.smoothingFn n` is the "smoothing function" 1/log(n), and `AkraBazziRecurrence.asympBound g a b n` is an asymptotic bound for the Akra-Bazzi recurrence. The theorem is a part of the proof for the upper bound of the Akra-Bazzi theorem, and the factor `1 - ε n` is included to ensure the induction step of the proof is valid.
More concisely: The theorem `AkraBazziRecurrence.T_isBigO_smoothingFn_mul_asympBound` in Lean 4 asserts that for any Akra-Bazzi recurrence `T`, the function `T` is asymptotically bounded above by `(1/log(n)) * (AkraBazziRecurrence.asympBound g a b n)`, where `g`, `a`, `b`, and `r` are given functions and `n` is the input size.
|
AkraBazziRecurrence.isLittleO_smoothingFn_one
theorem AkraBazziRecurrence.isLittleO_smoothingFn_one : AkraBazziRecurrence.smoothingFn =o[Filter.atTop] fun x => 1
This theorem, named `AkraBazziRecurrence.isLittleO_smoothingFn_one`, states that in the limit as x approaches infinity, the "smoothing function", which is defined as `1 / log(x)`, is little 'o' of the constant function `1`. This means that the smoothing function becomes insignificant relative to the constant function `1` as `x` tends to infinity. In mathematical terms, this is expressed as $\frac{1}{\log(x)} = o(1)$ as $x \rightarrow \infty$.
More concisely: As x approaches infinity, the smoothing function 1 / log(x) is little 'o' of the constant function 1, i.e., 1 / log(x) = o(1).
|
AkraBazziRecurrence.isBigO_symm_asympBound
theorem AkraBazziRecurrence.isBigO_symm_asympBound :
∀ {α : Type u_1} [inst : Fintype α] [inst_1 : Nonempty α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ},
AkraBazziRecurrence T g a b r → AkraBazziRecurrence.asympBound g a b =O[Filter.atTop] T
The theorem, known as the Akra-Bazzi theorem, states that for any given Akra-Bazzi recurrence `T` characterized by functions `a`, `b`, `g`, and `r`, the function `T` is bounded above (in big O notation) by the asymptotic bound of the Akra-Bazzi recurrence as `n` goes to infinity. In mathematical terms, `T` is in the set `Ω(n^p (1 + ∑_u^n g(u) / u^{p+1}))`, where `p` is a parameter associated with the recurrence. The theorem describes an important property of Akra-Bazzi recurrences, providing a bound on their behavior for large inputs.
More concisely: The Akra-Bazzi theorem asserts that for any given Akra-Bazzi recurrence `T` with functions `a`, `b`, `g`, and `r`, the upper bound of `T` in big O notation is `Ω(n^p (1 + ∑_u^n g(u) / u^{p+1}))`, where `p` is a constant related to the recurrence.
|
AkraBazziRecurrence.b_pos
theorem AkraBazziRecurrence.b_pos :
∀ {α : Type u_1} [inst : Fintype α] [inst_1 : Nonempty α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ},
AkraBazziRecurrence T g a b r → ∀ (i : α), 0 < b i
This theorem, `AkraBazziRecurrence.b_pos`, states that in the context of Akra-Bazzi recurrence relations, the elements of the `b` mapping are always positive. More specifically, given a type `α`, a function `T` from natural numbers to real numbers, a function `g` from real numbers to real numbers, mappings `a` and `b` from `α` to real numbers, and a mapping `r` from `α` and natural numbers to natural numbers such that they form an Akra-Bazzi recurrence, for any element `i` of type `α`, the value of `b` at `i` is strictly greater than zero.
More concisely: For any Akra-Bazzi recurrence relation with type `α`, real-valued functions `T`, `g`, `a`, and `b`, and natural number `i` of type `α`, the value `b(i)` is strictly positive.
|
AkraBazziRecurrence.isEquivalent_one_sub_smoothingFn_one
theorem AkraBazziRecurrence.isEquivalent_one_sub_smoothingFn_one :
Asymptotics.IsEquivalent Filter.atTop (fun x => 1 - AkraBazziRecurrence.smoothingFn x) fun x => 1
The theorem `AkraBazziRecurrence.isEquivalent_one_sub_smoothingFn_one` states that the function `1 - AkraBazziRecurrence.smoothingFn x` is asymptotically equivalent to the constant function `1` when `x` approaches infinity. In other words, as `x` gets larger and larger, the difference between `1 - AkraBazziRecurrence.smoothingFn x` and `1` (i.e., the negative of the smoothing function which is `1 / log x`) becomes negligible compared to `1`. In mathematical terms, it means that lim_{x → ∞} [1 - (1 / log x) - 1] / 1 = 0.
More concisely: The theorem `AkraBazziRecurrence.isEquivalent_one_sub_smoothingFn_one` asserts that the limit of `(1 - 1/log(x))/1` as `x` approaches infinity is equal to zero.
|
AkraBazziRecurrence.isTheta_asympBound
theorem AkraBazziRecurrence.isTheta_asympBound :
∀ {α : Type u_1} [inst : Fintype α] [inst_1 : Nonempty α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ},
AkraBazziRecurrence T g a b r → T =Θ[Filter.atTop] AkraBazziRecurrence.asympBound g a b
This theorem is known as the Akra-Bazzi theorem. It states that for any given Akra-Bazzi recurrence `T`, with respect to the function `g` and the coefficients `a` and `b`, and any `r`, if `T` is an Akra-Bazzi recurrence, then `T` belongs to the Theta class of the asymptotic bound function, denoted `n^p (1 + ∑_u^n g(u) / u^{p+1})`. This means that `T` grows at the same rate as the asymptotic bound function when `n` approaches infinity.
More concisely: The Akra-Bazzi recurrence `T` with function `g` and coefficients `a` and `b` is in Theta class with the asymptotic bound `n^p (1 + ∑_u^n g(u) / u^{p+1})`.
|
AkraBazziRecurrence.a_pos
theorem AkraBazziRecurrence.a_pos :
∀ {α : Type u_1} [inst : Fintype α] [inst_1 : Nonempty α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ},
AkraBazziRecurrence T g a b r → ∀ (i : α), 0 < a i
This theorem, `AkraBazziRecurrence.a_pos`, states that for any given type `α` that is a finite and nonempty set, and functions `T: ℕ → ℝ`, `g: ℝ → ℝ`, `a: α → ℝ`, `b: α → ℝ`, and `r: α → ℕ → ℕ` that satisfy the Akra-Bazzi recurrence, the values of function `a` at any `i` of type `α` are always positive, that is, `0 < a i` for all `i` of type `α`. In terms of mathematical symbols, given any `i ∈ α`, we have `a(i) > 0`.
More concisely: For any finite and nonempty set `α`, functions `T`, `g`, `a`, `b`, and `r` satisfying the Akra-Bazzi recurrence, we have `a(i) > 0` for all `i ∈ α`.
|