Polynomially bounded function

Conjectura.Defs.ComputerScience.Complexity.PolynomiallyBounded

/-
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
-/
import Mathlib.Algebra.Order.Group.Nat

/-! # Polynomially bounded function -/

namespace Conjectura.Complexity

/-- 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

end Conjectura.Complexity