AkraBazziRecurrence.GrowsPolynomially.pow
theorem AkraBazziRecurrence.GrowsPolynomially.pow :
∀ {f : ℝ → ℝ} (p : ℕ),
AkraBazziRecurrence.GrowsPolynomially f →
(∀ᶠ (x : ℝ) in Filter.atTop, 0 ≤ f x) → AkraBazziRecurrence.GrowsPolynomially fun x => f x ^ p
The theorem `AkraBazziRecurrence.GrowsPolynomially.pow` states that for any real function `f` and natural number `p`, if `f` grows polynomially (in the sense defined by `AkraBazziRecurrence.GrowsPolynomially`), and `f(x)` is nonnegative for all sufficiently large `x` (expressed as "eventually at top", denoted by `∀ᶠ (x : ℝ) in Filter.atTop, 0 ≤ f x`), then the function `f(x)^p` also grows polynomially. The growth of `f` is measured according to the Akra-Bazzi recurrence relation condition, i.e., there exist positive constants `c₁` and `c₂` such that `c₁ g(n) ≤ g(u) ≤ c₂ g(n)`, for `u` between `b*n` and `n` for any constant `b` in the open interval `(0,1)`.
More concisely: If `f` is a real function that grows polynomially and is nonnegative for all sufficiently large `x`, then `f(x)^p` also grows polynomially with the same polynomial degree as `f`.
|
AkraBazziRecurrence.GrowsPolynomially.rpow
theorem AkraBazziRecurrence.GrowsPolynomially.rpow :
∀ {f : ℝ → ℝ} (p : ℝ),
AkraBazziRecurrence.GrowsPolynomially f →
(∀ᶠ (x : ℝ) in Filter.atTop, 0 ≤ f x) → AkraBazziRecurrence.GrowsPolynomially fun x => f x ^ p
The theorem `AkraBazziRecurrence.GrowsPolynomially.rpow` states that for any real-valued function `f` and any real number `p`, if `f` satisfies the growth condition required by the Akra-Bazzi theorem (i.e., there exists constants `c₁` and `c₂` such that `c₁ f(n) ≤ f(u) ≤ c₂ f(n)` for any `u` in the range from `b*n` to `n`, where `b` is any constant in the open interval from 0 to 1), and if `f(x)` is nonnegative for sufficiently large `x`, then the function `g` defined by `g(x) = f(x) ^ p` also satisfies the Akra-Bazzi growth condition. This theorem allows us to apply the Akra-Bazzi method not only to `f` itself but also to any positive real power of `f`.
More concisely: If `f` is a real-valued function satisfying the Akra-Bazzi growth condition and is nonnegative for large `x`, then `g(x) = f(x) ^ p` also satisfies the Akra-Bazzi growth condition for any real number `p`.
|
AkraBazziRecurrence.GrowsPolynomially.inv
theorem AkraBazziRecurrence.GrowsPolynomially.inv :
∀ {f : ℝ → ℝ}, AkraBazziRecurrence.GrowsPolynomially f → AkraBazziRecurrence.GrowsPolynomially fun x => (f x)⁻¹
The theorem `AkraBazziRecurrence.GrowsPolynomially.inv` states that if a function `f`, mapping real numbers to real numbers, satisfies the Akra-Bazzi growth condition (i.e., `f` grows polynomially), then the reciprocal function `1 / f` also satisfies the same growth condition. In other words, for any given function `f`, if for every `b` in the open interval (0,1), there exist positive constants `c₁` and `c₂` such that for all sufficiently large `x`, `f(u)` lies between `c₁ * f(x)` and `c₂ * f(x)` for `u` between `b * x` and `x`, then the same property holds for the function `1 / f`, where `1 / f` is defined as `fun x => (f x)⁻¹`.
More concisely: If `f` is a real-valued function that grows polynomially according to the Akra-Bazzi condition, then the reciprocal function `1 / f` also satisfies the same condition.
|
AkraBazziRecurrence.GrowsPolynomially.congr_of_eventuallyEq
theorem AkraBazziRecurrence.GrowsPolynomially.congr_of_eventuallyEq :
∀ {f g : ℝ → ℝ},
Filter.atTop.EventuallyEq f g →
AkraBazziRecurrence.GrowsPolynomially g → AkraBazziRecurrence.GrowsPolynomially f
The theorem `AkraBazziRecurrence.GrowsPolynomially.congr_of_eventuallyEq` states that for any two real-valued functions `f` and `g`, if `f` is eventually equal to `g` at the limit towards infinity (that is `f =ᶠ[Filter.atTop] g`) and `g` satisfies the growth condition stipulated by the Akra-Bazzi theorem (that is, `AkraBazziRecurrence.GrowsPolynomially g`), then `f` also satisfies this growth condition (that is, `AkraBazziRecurrence.GrowsPolynomially f`). Essentially, it means that if `f` and `g` become the same for sufficiently large inputs and `g` grows polynomially under the Akra-Bazzi condition, then `f` also grows polynomially under the same condition.
More concisely: If real-valued functions `f` and `g` are eventually equal and `g` satisfies the Akra-Bazzi polynomial growth condition, then `f` also satisfies the same condition.
|
AkraBazziRecurrence.growsPolynomially_id
theorem AkraBazziRecurrence.growsPolynomially_id : AkraBazziRecurrence.GrowsPolynomially fun x => x
The theorem `AkraBazziRecurrence.growsPolynomially_id` states that the identity function `x` satisfies the Akra-Bazzi growth condition. In other words, for any constant `b` in the open interval `(0,1)`, there exist positive constants `c₁` and `c₂` such that for all sufficiently large `x`, for any `u` between `b*x` and `x`, `u` lies in the closed interval `[c₁*x, c₂*x]`. The identity function thus grows polynomially in accordance with the Akra-Bazzi theorem's requirement.
More concisely: For the identity function, there exist constants `c₁, c₂` such that for all sufficiently large `x`, any number `u` between `b*x` and `x` satisfies `c₁*x ≤ u ≤ c₂*x` for `0
|