theorem NLStrictPSPACE.nl_subset_space_log_squared {Γ : Type} (A : Set (List Γ)) (hA : LogSpace.InNL A) : SpaceComplexity.InSPACE (fun (n : ℕ) => Nat.log 2 n ^ 2) A

Theorem (Lecture 19). NL ⊆ SPACE(log² n). Any language in NL is decidable in deterministic space O((log n)²).

theorem NLStrictPSPACE.two_pow_gt_cube (m : ℕ) (hm : 10 ≤ m) : m ^ 3 < 2 ^ m

For every m ≥ 10, m³ < 2^m. Used to dominate c · (log₂ n)² by n asymptotically.

theorem NLStrictPSPACE.log_sq_little_o_id : SpaceComplexity.IsAsympDominated (fun (n : ℕ) => Nat.log 2 n ^ 2) fun (n : ℕ) => n

(log₂ n)² = o(n): the function n ↦ (Nat.log 2 n)² is asymptotically dominated by n. This is the key gap used to separate NL from PSPACE.

theorem NLStrictPSPACE.isAsympBoundedBy_trans_isAsympDominated {g h f : ℕ → ℕ} (hgh : SpaceComplexity.IsAsympBoundedBy g h) (hhf : SpaceComplexity.IsAsympDominated h f) : SpaceComplexity.IsAsympDominated g f

If g = O(h) and h = o(f), then g = o(f): composing a Big-O bound with a little-o bound yields a little-o bound.

theorem NLStrictPSPACE.log_sq_le_sq (n : ℕ) : Nat.log 2 n ^ 2 ≤ n ^ 2

Trivial pointwise bound: (log₂ n)² ≤ n² for all n.

theorem NLStrictPSPACE.space_log_sq_subset_pspace {Γ : Type} (A : Set (List Γ)) (hA : SpaceComplexity.InSPACE (fun (n : ℕ) => Nat.log 2 n ^ 2) A) : SpaceComplexity.InPSPACE A

SPACE((log₂ n)²) ⊆ PSPACE: any language decidable in space (log₂ n)² is decidable in polynomial space (in particular, in space n²).

theorem NLStrictPSPACE.nl_subset_pspace {Γ : Type} (A : Set (List Γ)) (hA : LogSpace.InNL A) : SpaceComplexity.InPSPACE A

NL ⊆ PSPACE. Combines NL ⊆ SPACE(log² n) with SPACE(log² n) ⊆ PSPACE.

theorem NLStrictPSPACE.log_sq_little_o_succ2 : SpaceComplexity.IsAsympDominated (fun (n : ℕ) => Nat.log 2 n ^ 2) fun (n : ℕ) => n + 2

(log₂ n)² = o(n + 2). Combined with the Space Hierarchy Theorem at bound n + 2, this lets us separate SPACE(n + 2) from NL ⊆ SPACE(log² n).

theorem NLStrictPSPACE.space_log_sq_in_spaceo_succ2 {Γ : Type} (A : Set (List Γ)) (hA : SpaceComplexity.InSPACE (fun (n : ℕ) => Nat.log 2 n ^ 2) A) : SpaceComplexity.InSPACEo (fun (n : ℕ) => n + 2) A

A language decidable in space (log₂ n)² is decidable in space o(n + 2), i.e. it lies in SPACEo (n + 2).

theorem NLStrictPSPACE.succ2_space_constructible : SpaceComplexity.SpaceConstructible fun (n : ℕ) => n + 2

The function n ↦ n + 2 is space-constructible. This is the technical hypothesis needed to apply the Space Hierarchy Theorem at this bound.

theorem NLStrictPSPACE.space_succ2_subset_pspace {Γ : Type} (A : Set (List Γ)) (hA : SpaceComplexity.InSPACE (fun (n : ℕ) => n + 2) A) : SpaceComplexity.InPSPACE A

SPACE(n + 2) ⊆ PSPACE. Linear space is contained in polynomial space (in particular n²).

theorem NLStrictPSPACE.nl_ssubset_pspace {Γ : Type} [Inhabited Γ] : (∀ (A : Set (List Γ)), LogSpace.InNL A → SpaceComplexity.InPSPACE A) ∧ ∃ (A : Set (List Γ)), SpaceComplexity.InPSPACE A ∧ ¬LogSpace.InNL A

Corollary (Sipser, Review of Hierarchy Theorems). NL ⊊ PSPACE.

Concretely we prove the two parts of strict inclusion:

1. Every NL language lies in PSPACE.
2. There exists a PSPACE language not in NL, obtained from the Space Hierarchy Theorem at the bound n + 2 (which is space-constructible). Any NL language is in SPACE(log² n), hence in SPACEo(n + 2), contradicting the hierarchy separation.