Documentation

Mathlib.Computability.AkraBazzi.GrowsPolynomially

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 Akra-Bazzi 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 states that the condition must hold for any b ∈ (0,1). This is equivalent to only requiring it for b = 1/2 or any other particular value between 0 and 1. While this could in principle make it harder to prove that a particular function grows polynomially, this issue doesn't seem to arise in practice.

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
Instances For
    theorem AkraBazziRecurrence.GrowsPolynomially.eventually_atTop_le {f : } {b : } (hb : b Set.Ioo 0 1) (hf : AkraBazziRecurrence.GrowsPolynomially f) :
    ∃ c > 0, ∀ᶠ (x : ) in Filter.atTop, uSet.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 : AkraBazziRecurrence.GrowsPolynomially f) :
    ∃ c > 0, ∀ᶠ (n : ) in Filter.atTop, uSet.Icc (b * n) n, f u c * f n
    theorem AkraBazziRecurrence.GrowsPolynomially.eventually_atTop_ge {f : } {b : } (hb : b Set.Ioo 0 1) (hf : AkraBazziRecurrence.GrowsPolynomially f) :
    ∃ c > 0, ∀ᶠ (x : ) in Filter.atTop, uSet.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 : AkraBazziRecurrence.GrowsPolynomially f) :
    ∃ c > 0, ∀ᶠ (n : ) in Filter.atTop, uSet.Icc (b * n) n, c * f n f u
    theorem AkraBazziRecurrence.GrowsPolynomially.eventually_zero_of_frequently_zero {f : } (hf : AkraBazziRecurrence.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 : AkraBazziRecurrence.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 : AkraBazziRecurrence.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.add {f : } {g : } (hf : AkraBazziRecurrence.GrowsPolynomially f) (hg : AkraBazziRecurrence.GrowsPolynomially g) (hf' : 0 ≤ᶠ[Filter.atTop] f) (hg' : 0 ≤ᶠ[Filter.atTop] g) :
    theorem AkraBazziRecurrence.GrowsPolynomially.rpow {f : } (p : ) (hf : AkraBazziRecurrence.GrowsPolynomially f) (hf_nonneg : ∀ᶠ (x : ) in Filter.atTop, 0 f x) :
    theorem AkraBazziRecurrence.GrowsPolynomially.pow {f : } (p : ) (hf : AkraBazziRecurrence.GrowsPolynomially f) (hf_nonneg : ∀ᶠ (x : ) in Filter.atTop, 0 f x) :
    theorem AkraBazziRecurrence.GrowsPolynomially.zpow {f : } (p : ) (hf : AkraBazziRecurrence.GrowsPolynomially f) (hf_nonneg : ∀ᶠ (x : ) in Filter.atTop, 0 f x) :
    theorem AkraBazziRecurrence.GrowsPolynomially.of_isTheta {f : } {g : } (hg : AkraBazziRecurrence.GrowsPolynomially g) (hf : f =Θ[Filter.atTop] g) (hf' : ∀ᶠ (x : ) in Filter.atTop, 0 f x) :