Polynomially bounded functions

8 fully proved

Polynomially Bounded

TheoremPolynomial bounds with equal coefficient and exponent#✓fully proved

Polynomial growth is equivalent to a global bound whose coefficient equals its exponent.

theorem polynomiallyBounded_iff_le_mul_pow_self {f : ℕ → ℕ} :
    PolynomiallyBounded f ↔ ∃ c : ℕ, ∀ n, f n ≤ c * (n + 1) ^ c

Used by 6

Used bySums of polynomially bounded functions are polynomially bounded · Compositions of polynomially bounded functions are polynomially bounded · Constant functions are polynomially bounded · The identity function is polynomially bounded · The normalized polynomial bound is polynomially bounded and monotone · Products of polynomially bounded functions are polynomially bounded

TheoremConstant functions are polynomially bounded#✓fully proved

Every constant natural-valued function is polynomially bounded.

theorem const (a : ℕ) : PolynomiallyBounded (fun _ ↦ a)

Uses 1 · Used by 1

Proof usesPolynomial bounds with equal coefficient and exponent

Used byPowers of polynomially bounded functions are polynomially bounded

TheoremThe identity function is polynomially bounded#✓fully proved

The identity function on natural numbers is polynomially bounded.

theorem id : PolynomiallyBounded (fun n ↦ n)

Uses 1

Proof usesPolynomial bounds with equal coefficient and exponent

TheoremSums of polynomially bounded functions are polynomially bounded#✓fully proved

A pointwise sum of polynomially bounded functions is polynomially bounded.

theorem add (hf : PolynomiallyBounded f) (hg : PolynomiallyBounded g) :
    PolynomiallyBounded (fun n ↦ f n + g n)

Uses 1

Proof usesPolynomial bounds with equal coefficient and exponent

TheoremProducts of polynomially bounded functions are polynomially bounded#✓fully proved

A pointwise product of polynomially bounded functions is polynomially bounded.

theorem mul (hf : PolynomiallyBounded f) (hg : PolynomiallyBounded g) :
    PolynomiallyBounded (fun n ↦ f n * g n)

Uses 1 · Used by 1

Proof usesPolynomial bounds with equal coefficient and exponent

Used byPowers of polynomially bounded functions are polynomially bounded

TheoremPowers of polynomially bounded functions are polynomially bounded#✓fully proved

A fixed pointwise power of a polynomially bounded function is polynomially bounded.

theorem pow (hf : PolynomiallyBounded f) (k : ℕ) :
    PolynomiallyBounded (fun n ↦ f n ^ k)

Uses 2

Proof usesConstant functions are polynomially bounded · Products of polynomially bounded functions are polynomially bounded

TheoremCompositions of polynomially bounded functions are polynomially bounded#✓fully proved

A composition of polynomially bounded functions is polynomially bounded.

theorem comp (hf : PolynomiallyBounded f) (hg : PolynomiallyBounded g) :
    PolynomiallyBounded (fun n ↦ f (g n))

Uses 1

Proof usesPolynomial bounds with equal coefficient and exponent

TheoremThe normalized polynomial bound is polynomially bounded and monotone#✓fully proved

The normalized bound is itself polynomially bounded and monotone in its input.

theorem mono_bound (c : ℕ) :
    PolynomiallyBounded (fun n ↦ c * (n + 1) ^ c) ∧
      Monotone (fun n ↦ c * (n + 1) ^ c)

Uses 1

Proof usesPolynomial bounds with equal coefficient and exponent

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.