Polynomial time as charged asymptotic bounds

A function computable in polynomial time is computable within charged bounds O(T) and O(S) that are polynomial in the length of the encoded input. The time bound is the time of a realizing machine; the space bound is the sum of its time and space, since the charged space also bounds the length of the encoded output, which the machine's time bounds.

Main results

• Turing.MultiTapeTM.ComputableInPolyTime.exists_computableInO: polynomial time gives polynomial charged bounds.

theorem Turing.MultiTapeTM.ComputableInPolyTime.exists_computableInO {α : Type u_1} {β : Type u_2} {f : α → β} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} (h : ComputableInPolyTime f encIn encOut) : ∃ (T : α → ℕ) (S : α → ℕ), PolyBounded (fun (a : α) => (encIn a).length) T ∧ PolyBounded (fun (a : α) => (encIn a).length) S ∧ ComputableInO f encIn encOut T S

Polynomial time gives polynomial charged bounds: a function computable in polynomial time is computable within time O(T) and space O(S) for bounds polynomial in the length of the encoded input, namely the time of a realizing machine and the sum of its time and space.