Akra-Bazzi theorem: The polynomial growth condition

This file defines and develops an API for the polynomial growth condition that appears in the statement of the Akra-Bazzi theorem: for the theorem to hold, the function g must satisfy the condition that c₁ g(n) ≤ g(u) ≤ c₂ g(n), for u between b*n and n for any constant b ∈ (0,1).

Implementation notes

Our definition requires that the condition must hold for any b ∈ (0,1). This is equivalent to requiring it for b = 1 / 2 (or any other particular value in (0, 1)). While this could, in principle, make it harder to prove that a particular function grows polynomially, this issue does not seem to arise in practice.

def AkraBazziRecurrence.GrowsPolynomially (f : ℝ → ℝ) : Prop

The growth condition that the function g must satisfy for the Akra-Bazzi 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).

Equations

• AkraBazziRecurrence.GrowsPolynomially f = ∀ b ∈ Set.Ioo 0 1, ∃ c₁ > 0, ∃ c₂ > 0, ∀ᶠ (x : ℝ) in Filter.atTop, ∀ u ∈ Set.Icc (b * x) x, f u ∈ Set.Icc (c₁ * f x) (c₂ * f x)

theorem AkraBazziRecurrence.GrowsPolynomially.congr_of_eventuallyEq {f g : ℝ → ℝ} (hfg : f =ᶠ[Filter.atTop] g) (hg : GrowsPolynomially g) : GrowsPolynomially f

theorem AkraBazziRecurrence.GrowsPolynomially.iff_eventuallyEq {f g : ℝ → ℝ} (h : f =ᶠ[Filter.atTop] g) : GrowsPolynomially f ↔ GrowsPolynomially g

theorem AkraBazziRecurrence.GrowsPolynomially.eventually_atTop_le {f : ℝ → ℝ} {b : ℝ} (hb : b ∈ Set.Ioo 0 1) (hf : GrowsPolynomially f) : ∃ c > 0, ∀ᶠ (x : ℝ) in Filter.atTop, ∀ u ∈ Set.Icc (b * x) x, f u ≤ c * f x

theorem AkraBazziRecurrence.GrowsPolynomially.eventually_atTop_le_nat {f : ℝ → ℝ} {b : ℝ} (hb : b ∈ Set.Ioo 0 1) (hf : GrowsPolynomially f) : ∃ c > 0, ∀ᶠ (n : ℕ) in Filter.atTop, ∀ u ∈ Set.Icc (b * ↑n) ↑n, f u ≤ c * f ↑n

theorem AkraBazziRecurrence.GrowsPolynomially.eventually_atTop_ge {f : ℝ → ℝ} {b : ℝ} (hb : b ∈ Set.Ioo 0 1) (hf : GrowsPolynomially f) : ∃ c > 0, ∀ᶠ (x : ℝ) in Filter.atTop, ∀ u ∈ Set.Icc (b * x) x, c * f x ≤ f u

theorem AkraBazziRecurrence.GrowsPolynomially.eventually_atTop_ge_nat {f : ℝ → ℝ} {b : ℝ} (hb : b ∈ Set.Ioo 0 1) (hf : GrowsPolynomially f) : ∃ c > 0, ∀ᶠ (n : ℕ) in Filter.atTop, ∀ u ∈ Set.Icc (b * ↑n) ↑n, c * f ↑n ≤ f u

theorem AkraBazziRecurrence.GrowsPolynomially.eventually_zero_of_frequently_zero {f : ℝ → ℝ} (hf : GrowsPolynomially f) (hf' : ∃ᶠ (x : ℝ) in Filter.atTop, f x = 0) : ∀ᶠ (x : ℝ) in Filter.atTop, f x = 0

theorem AkraBazziRecurrence.GrowsPolynomially.eventually_atTop_nonneg_or_nonpos {f : ℝ → ℝ} (hf : GrowsPolynomially f) : (∀ᶠ (x : ℝ) in Filter.atTop, 0 ≤ f x) ∨ ∀ᶠ (x : ℝ) in Filter.atTop, f x ≤ 0

theorem AkraBazziRecurrence.GrowsPolynomially.eventually_atTop_zero_or_pos_or_neg {f : ℝ → ℝ} (hf : GrowsPolynomially f) : (∀ᶠ (x : ℝ) in Filter.atTop, f x = 0) ∨ (∀ᶠ (x : ℝ) in Filter.atTop, 0 < f x) ∨ ∀ᶠ (x : ℝ) in Filter.atTop, f x < 0

theorem AkraBazziRecurrence.GrowsPolynomially.neg {f : ℝ → ℝ} (hf : GrowsPolynomially f) : GrowsPolynomially (-f)

theorem AkraBazziRecurrence.GrowsPolynomially.neg_iff {f : ℝ → ℝ} : GrowsPolynomially f ↔ GrowsPolynomially (-f)

theorem AkraBazziRecurrence.GrowsPolynomially.abs {f : ℝ → ℝ} (hf : GrowsPolynomially f) : GrowsPolynomially fun (x : ℝ) => |f x|

theorem AkraBazziRecurrence.GrowsPolynomially.norm {f : ℝ → ℝ} (hf : GrowsPolynomially f) : GrowsPolynomially fun (x : ℝ) => ‖f x‖

theorem AkraBazziRecurrence.growsPolynomially_const {c : ℝ} : GrowsPolynomially fun (x : ℝ) => c

theorem AkraBazziRecurrence.growsPolynomially_id : GrowsPolynomially fun (x : ℝ) => x

theorem AkraBazziRecurrence.GrowsPolynomially.mul {f g : ℝ → ℝ} (hf : GrowsPolynomially f) (hg : GrowsPolynomially g) : GrowsPolynomially fun (x : ℝ) => f x * g x

theorem AkraBazziRecurrence.GrowsPolynomially.const_mul {f : ℝ → ℝ} {c : ℝ} (hf : GrowsPolynomially f) : GrowsPolynomially fun (x : ℝ) => c * f x

theorem AkraBazziRecurrence.GrowsPolynomially.add {f g : ℝ → ℝ} (hf : GrowsPolynomially f) (hg : GrowsPolynomially g) (hf' : 0 ≤ᶠ[Filter.atTop] f) (hg' : 0 ≤ᶠ[Filter.atTop] g) : GrowsPolynomially fun (x : ℝ) => f x + g x

theorem AkraBazziRecurrence.GrowsPolynomially.add_isLittleO {f g : ℝ → ℝ} (hf : GrowsPolynomially f) (hfg : g =o[Filter.atTop] f) : GrowsPolynomially fun (x : ℝ) => f x + g x

theorem AkraBazziRecurrence.GrowsPolynomially.inv {f : ℝ → ℝ} (hf : GrowsPolynomially f) : GrowsPolynomially fun (x : ℝ) => (f x)⁻¹

theorem AkraBazziRecurrence.GrowsPolynomially.div {f g : ℝ → ℝ} (hf : GrowsPolynomially f) (hg : GrowsPolynomially g) : GrowsPolynomially fun (x : ℝ) => f x / g x

theorem AkraBazziRecurrence.GrowsPolynomially.rpow {f : ℝ → ℝ} (p : ℝ) (hf : GrowsPolynomially f) (hf_nonneg : ∀ᶠ (x : ℝ) in Filter.atTop, 0 ≤ f x) : GrowsPolynomially fun (x : ℝ) => f x ^ p

theorem AkraBazziRecurrence.GrowsPolynomially.pow {f : ℝ → ℝ} (p : ℕ) (hf : GrowsPolynomially f) (hf_nonneg : ∀ᶠ (x : ℝ) in Filter.atTop, 0 ≤ f x) : GrowsPolynomially fun (x : ℝ) => f x ^ p

theorem AkraBazziRecurrence.GrowsPolynomially.zpow {f : ℝ → ℝ} (p : ℤ) (hf : GrowsPolynomially f) (hf_nonneg : ∀ᶠ (x : ℝ) in Filter.atTop, 0 ≤ f x) : GrowsPolynomially fun (x : ℝ) => f x ^ p

theorem AkraBazziRecurrence.growsPolynomially_rpow (p : ℝ) : GrowsPolynomially fun (x : ℝ) => x ^ p

theorem AkraBazziRecurrence.growsPolynomially_pow (p : ℕ) : GrowsPolynomially fun (x : ℝ) => x ^ p

theorem AkraBazziRecurrence.growsPolynomially_zpow (p : ℤ) : GrowsPolynomially fun (x : ℝ) => x ^ p

theorem AkraBazziRecurrence.growsPolynomially_log : GrowsPolynomially Real.log

theorem AkraBazziRecurrence.GrowsPolynomially.of_isTheta {f g : ℝ → ℝ} (hg : GrowsPolynomially g) (hf : f =Θ[Filter.atTop] g) (hf' : ∀ᶠ (x : ℝ) in Filter.atTop, 0 ≤ f x) : GrowsPolynomially f

theorem AkraBazziRecurrence.GrowsPolynomially.of_isEquivalent {f g : ℝ → ℝ} (hg : GrowsPolynomially g) (hf : Asymptotics.IsEquivalent Filter.atTop f g) : GrowsPolynomially f

theorem AkraBazziRecurrence.GrowsPolynomially.of_isEquivalent_const {f : ℝ → ℝ} {c : ℝ} (hf : Asymptotics.IsEquivalent Filter.atTop f fun (x : ℝ) => c) : GrowsPolynomially f