Polynomial growth relative to an arbitrary input-size function, without machine predicates.

Polynomial bounds

def Turing.MultiTapeTM.PolyBounded {α : Type u_1} (size u : α → ℕ) : Prop

u is bounded by a polynomially bounded function of size. This adapts Cslib.PolynomiallyBounded to arbitrary inputs; it does not assert computability.

theorem Turing.MultiTapeTM.PolyBounded.exists_le {α : Type u_1} {size u : α → ℕ} (h : PolyBounded size u) : ∃ (c : ℕ) (d : ℕ), ∀ (a : α), u a ≤ c * (size a + 1) ^ d

Recover an explicit polynomial bound valid at every input, including size zero.

theorem Turing.MultiTapeTM.PolyBounded.of_forall_le {α : Type u_1} {size u : α → ℕ} (c d : ℕ) (h : ∀ (a : α), u a ≤ c * (size a + 1) ^ d) : PolyBounded size u

Supply an explicit polynomial bound in the input size.

theorem Turing.MultiTapeTM.PolyBounded.of_polynomiallyBounded {α : Type u_1} (size : α → ℕ) {bound : ℕ → ℕ} (hbound : Cslib.PolynomiallyBounded bound) : PolyBounded size fun (a : α) => bound (size a)

Apply a polynomial bound to any input-size function.

theorem Turing.MultiTapeTM.PolyBounded.polynomiallyBounded {f : ℕ → ℕ} (h : PolyBounded id f) : Cslib.PolynomiallyBounded f

With the identity size, the adapter gives CSLib's polynomial-growth predicate.

theorem Turing.MultiTapeTM.PolyBounded.mono {α : Type u_1} {size u v : α → ℕ} (h : PolyBounded size v) (huv : ∀ (a : α), u a ≤ v a) : PolyBounded size u

theorem Turing.MultiTapeTM.PolyBounded.const {α : Type u_1} {size : α → ℕ} (k : ℕ) : PolyBounded size fun (x : α) => k

theorem Turing.MultiTapeTM.PolyBounded.self {α : Type u_1} {size : α → ℕ} : PolyBounded size size

theorem Turing.MultiTapeTM.PolyBounded.add {α : Type u_1} {size u v : α → ℕ} (hu : PolyBounded size u) (hv : PolyBounded size v) : PolyBounded size fun (a : α) => u a + v a

theorem Turing.MultiTapeTM.PolyBounded.mul {α : Type u_1} {size u v : α → ℕ} (hu : PolyBounded size u) (hv : PolyBounded size v) : PolyBounded size fun (a : α) => u a * v a

theorem Turing.MultiTapeTM.PolyBounded.pow {α : Type u_1} {size u : α → ℕ} (hu : PolyBounded size u) (d : ℕ) : PolyBounded size fun (a : α) => u a ^ d

theorem Turing.MultiTapeTM.PolyBounded.comp {α : Type u_1} {β : Type u_2} {size : α → ℕ} {size' v : β → ℕ} {g : α → β} (hv : PolyBounded size' v) (hg : PolyBounded size fun (a : α) => size' (g a)) : PolyBounded size fun (a : α) => v (g a)

Substitution: if v is bounded by a polynomial in size' and size' ∘ g by a polynomial in size, then v ∘ g is bounded by a polynomial in size.