Polynomial degree bounds in an arbitrary size measure

These bounds and their arithmetic are independent of machine computability.

Main definitions

• Turing.MultiTapeTM.DegreeBounded: a bound by a constant times (size + 1) ^ d.

Main results

• DegreeBounded.add_max, DegreeBounded.mul, DegreeBounded.comp: arithmetic of degree bounds.

Bounds of a given degree

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

u is bounded by a polynomial of degree d in size.

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

theorem Turing.MultiTapeTM.DegreeBounded.mono_deg {α : Type u_1} {size u : α → ℕ} {d₁ d₂ : ℕ} (h : DegreeBounded size u d₁) (hd : d₁ ≤ d₂) : DegreeBounded size u d₂

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

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

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

theorem Turing.MultiTapeTM.DegreeBounded.add_max {α : Type u_1} {size u v : α → ℕ} {d₁ d₂ : ℕ} (hu : DegreeBounded size u d₁) (hv : DegreeBounded size v d₂) : DegreeBounded size (fun (a : α) => u a + v a) (max d₁ d₂)

Adding bounds of different degrees gives a bound of their maximum degree.

theorem Turing.MultiTapeTM.DegreeBounded.smul {α : Type u_1} {size u : α → ℕ} {d : ℕ} (k : ℕ) (hu : DegreeBounded size u d) : DegreeBounded size (fun (a : α) => k * u a) d

theorem Turing.MultiTapeTM.DegreeBounded.add_const {α : Type u_1} {size u : α → ℕ} {d : ℕ} (k : ℕ) (hu : DegreeBounded size u d) : DegreeBounded size (fun (a : α) => u a + k) d

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

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

Substitution: if v has degree d₂ in size' and size' ∘ g has degree d₁ in size, then v ∘ g has degree d₁ * d₂ in size.

theorem Turing.MultiTapeTM.DegreeBounded.polyBounded {α : Type u_1} {size u : α → ℕ} {d : ℕ} (h : DegreeBounded size u d) : PolyBounded size u