P — surface layer

This file aggregates the definitions and theorems for P, FP, and PSPACE.

Definitions (from P/Defs.lean)

• P — polynomial time: ⋃ k, DTIME(n^k)
• FP — functions computable in polynomial time
• PSPACE — polynomial space: ⋃ k, DSPACE(n^k)

Theorems

• DTIME_union — DTIME is closed under union (AB Claim 1.5)

theorem Complexity.DTIME_union {T₁ T₂ : ℕ → ℕ} {L₁ L₂ : Language} (h₁ : L₁ ∈ DTIME T₁) (h₂ : L₂ ∈ DTIME T₂) : L₁ ∪ L₂ ∈ DTIME fun (n : ℕ) => T₁ n + T₂ n

DTIME is closed under union (AB Claim 1.5): if L₁ ∈ DTIME(T₁) and L₂ ∈ DTIME(T₂), then L₁ ∪ L₂ ∈ DTIME(T₁ + T₂).