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

Savitch's theorem at the log-space level. If a language A is decidable by a nondeterministic TM in space O(log n), then it is decidable by a deterministic TM in space O((log n)²). This is the instance of Savitch's theorem NSPACE(f) ⊆ SPACE(f²) with f(n) = log n, used to derive NL ⊆ SPACE(log² n).

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

NL ⊆ SPACE(log² n). Every language decidable in nondeterministic logarithmic space is decidable in O((log n)²) deterministic space. Immediate consequence of savitch_log applied to the definition InNL A := InNSPACE log A.