Conjectura
Sign inRegister
Beta.Proofs cannot be submitted yet. The corpus is open to read, and we are looking for researchers to maintain a subject area.Maintaining a field →

Polynomially bounded function

PolynomiallyBoundeddef

A function is polynomially bounded when some polynomial dominates it everywhere. This is the growth class that separates "feasible" from "infeasible" in complexity theory.

def PolynomiallyBounded (f : ℕ → ℕ) : Prop :=
  ∃ c k : ℕ, ∀ n : ℕ, f n ≤ c * n ^ k + c

From Mathlib

import Conjectura.Defs.ComputerScience.Complexity.PolynomiallyBounded · maintainer — open · raw source

Copyright (c) 2026 The Conjectura Authors. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: The Conjectura Authors

Full credits