InformationTheory.Shannon.Kolmogorov.Invariance

Imports 2

Invariance and the literal upper bound #

complexity_le_natLen — the literal echo program gives C(x) ≤ natLen x + O(1).
invariance_code — for any fixed code c, a description of x via c is matched by the universal machine up to a constant number of extra bits.
invariance — the same for an arbitrary partial recursive description method A, obtained from invariance_code through exists_code.

The additive constant is explicit: prepending the interpret selector for a code index idx costs idx + 2 bits, and the literal flag costs one bit.

theorem

InformationTheory.Kolmogorov.complexity_le_natLen

source

∃ (c : ℕ), ∀ (x : ℕ), complexity x ≤ natLen x + c

Literal upper bound: the echo program false :: encodeNat x describes x, so C(x) ≤ natLen x + 1. @audit:ok

Used by

theorem

InformationTheory.Kolmogorov.invariance_code

source

(c : Nat.Partrec.Code) :

∃ (b : ℕ), ∀ (x y : ℕ) (q : List Bool), x ∈ c.eval (Nat.pair (Computability.decodeNat q) y) → condComplexity x y ≤ q.length + b

Invariance against a fixed code c: any bit-string description q with x ∈ eval c (Nat.pair (decodeNat q) y) yields C(x | y) ≤ q.length + b, with b = encodeCode c + 2 independent of x, y, q. @audit:ok

Used by

theorem

InformationTheory.Kolmogorov.invariance

source

(A : ℕ → ℕ → Part ℕ) (hA : Partrec₂ A) :

∃ (b : ℕ), ∀ (x y : ℕ) (q : List Bool), x ∈ A (Computability.decodeNat q) y → condComplexity x y ≤ q.length + b

Invariance against an arbitrary partial recursive description method A: C(x | y) ≤ (A-description length) + b for a constant b. @audit:ok

Used by