Skip to content

InformationTheory.Shannon.Kolmogorov.Levin

Imports 4

Prefix complexity and universal probability: the factor-two relation #

The self-delimiting machine prefixUniversalEval accepts a program only when its unary length prefix matches the length of its payload, so every accepted program is selfDelimit d for its payload d, of length 2 * d.length + 1. Prefix complexity is therefore rigidly tied to the shortest payload length payloadComplexity x by prefixComplexity x = 2 * payloadComplexity x + 1, and the two-sided relation between prefixComplexity and universalProb carries that same factor of two:

-log₂ P_U(x) ≤ K(x) ≤ 2 * (-log₂ P_U(x)) + 1.

The left inequality is neg_logb_universalProb_le_prefixComplexity; the right one is prefixComplexity_le_two_mul_neg_logb_universalProb, proved here by counting. The programs producing x inject into the payloads of length at least payloadComplexity x, and re-wrapping such a payload with a unary prefix shortened by payloadComplexity x (the map padDelimit) exhibits the weight 2^{-(2|d|+1)} as 2^{-payloadComplexity x} times a Kraft-summable weight over a prefix-free set.

Main definitions #

payloadComplexity — the length of the shortest payload describing x.
padDelimit — the unary length-prefix wrapper with the run of trues shortened by a fixed offset.

Main statements #

prefixComplexity_eq_two_mul_payloadComplexity_add_one — the structural identity K(x) = 2 * m(x) + 1 for the shortest payload length m(x).
universalProb_le_two_pow_neg_payloadComplexity — the counting bound P_U(x) ≤ 2^{-m(x)}.
prefixComplexity_le_two_mul_neg_logb_universalProb — the upper half of the factor-two relation, K(x) ≤ 2 * (-log₂ P_U(x)) + 1.

Implementation notes #

The factor two is a property of this machine rather than an artifact of the argument: it is forced by the shape of the accepted programs, since a payload of length n can only be presented as a program of length 2 * n + 1. The additive coding theorem K(x) = -log₂ P_U(x) + O(1) is a statement about additively universal prefix machines — those able to simulate any other prefix machine at a cost bounded by a constant — and is not claimed here.

The offset wrapper padDelimit m is deliberately not a program of the machine for m ≠ 0: its unary prefix undercounts its payload, so the acceptance guard rejects it. Only prefix-freeness of its image is needed, which is why the Kraft bound is used in the form PrefixFree.tsum_inv_two_pow_length_le_one, stated for an arbitrary prefix-free set rather than for the machine's domain.

References #

The universal probability and its relation to prefix complexity follow Cover–Thomas (2nd ed.).

Tags #

Kolmogorov complexity, prefix complexity, universal probability, coding theorem

noncomputable def

InformationTheory.Kolmogorov.payloadComplexity

(x : ℕ) :

The payload complexity of x: the length of the shortest payload d that decodes to x. Every accepted program of prefixUniversalEval is selfDelimit of its payload, so this is the complexity measure the machine actually minimizes, up to the self-delimiting overhead. @audit:ok

Equations

InformationTheory.Kolmogorov.payloadComplexity x = sInf {l : ℕ | ∃ (d : List Bool), d.length = l ∧ x ∈ InformationTheory.Kolmogorov.decodePayload d}

Instances For

Used by

def

InformationTheory.Kolmogorov.padDelimit

(m : ℕ) (d : List Bool) :

The self-delimiting wrapper with its unary run of trues shortened by the offset m: replicate (d.length - m) true ++ false :: d. For m ≤ d.length the images over all payloads still form a prefix-free set, while each codeword is shorter than selfDelimit d by exactly m. @audit:ok

Equations

InformationTheory.Kolmogorov.padDelimit m d = List.replicate (d.length - m) true ++ false :: d

Instances For

Used by

theorem

InformationTheory.Kolmogorov.prefixUniversalEval_selfDelimit

(d : List Bool) :

prefixUniversalEval (selfDelimit d) = decodePayload d

Used by

theorem

InformationTheory.Kolmogorov.selfDelimit_parseUnary_snd_of_mem

{x : ℕ} {p : List Bool} (h : x ∈ prefixUniversalEval p) :

selfDelimit (parseUnary p).2 = p

Used by

theorem

InformationTheory.Kolmogorov.payloadComplexity_set_nonempty

(x : ℕ) :

{l : ℕ | ∃ (d : List Bool), d.length = l ∧ x ∈ decodePayload d}.Nonempty

Used by

theorem

InformationTheory.Kolmogorov.payloadComplexity_spec

(x : ℕ) :

∃ (d : List Bool), d.length = payloadComplexity x ∧ x ∈ decodePayload d

Used by

theorem

InformationTheory.Kolmogorov.payloadComplexity_le_of_mem

{x : ℕ} {d : List Bool} (h : x ∈ decodePayload d) :

payloadComplexity x ≤ d.length

Used by

theorem

InformationTheory.Kolmogorov.prefixComplexity_eq_two_mul_payloadComplexity_add_one

(x : ℕ) :

prefixComplexity x = 2 * payloadComplexity x + 1

Prefix complexity is rigidly determined by the shortest payload length, K(x) = 2 * m(x) + 1, because every accepted program is selfDelimit of its payload and selfDelimit doubles the payload length. @audit:ok

Used by

theorem

InformationTheory.Kolmogorov.parseUnary_padDelimit

(m : ℕ) (d : List Bool) :

parseUnary (padDelimit m d) = (d.length - m, d)

Used by

theorem

InformationTheory.Kolmogorov.padDelimit_length

{m : ℕ} {d : List Bool} (h : m ≤ d.length) :

(padDelimit m d).length = 2 * d.length + 1 - m

Used by

theorem

InformationTheory.Kolmogorov.padDelimit_injective

(m : ℕ) :

Function.Injective (padDelimit m)

Used by

theorem

InformationTheory.Kolmogorov.padDelimit_image_prefixFree

(m : ℕ) :

PrefixFree (padDelimit m '' {d : List Bool | m ≤ d.length})

Used by

theorem

InformationTheory.Kolmogorov.nil_not_mem_padDelimit_image

(m : ℕ) :

[] ∉ padDelimit m '' {d : List Bool | m ≤ d.length}

Used by

theorem

InformationTheory.Kolmogorov.tsum_inv_two_pow_padDelimit_length_le_one

(m : ℕ) :

∑' (d : { d : List Bool // m ≤ d.length }), 2⁻¹ ^ (padDelimit m ↑d).length ≤ 1

Used by

theorem

InformationTheory.Kolmogorov.universalProb_le_two_pow_neg_payloadComplexity

(x : ℕ) :

universalProb x ≤ 2⁻¹ ^ payloadComplexity x

The counting bound P_U(x) ≤ 2^{-m(x)} for the shortest payload length m(x): the programs producing x inject into the payloads of length at least m(x), whose weights are 2^{-m(x)} times a Kraft-summable family. @audit:ok

Used by

theorem

InformationTheory.Kolmogorov.prefixComplexity_le_two_mul_neg_logb_universalProb

(x : ℕ) :

↑(prefixComplexity x) ≤ 2 * -Real.logb 2 (universalProb x).toReal + 1

The upper half of the factor-two relation between prefix complexity and universal probability: K(x) ≤ 2 * (-log₂ P_U(x)) + 1. Together with neg_logb_universalProb_le_prefixComplexity this places K(x) between -log₂ P_U(x) and twice that value plus one. The bound is not the degenerate logb 2 0 = 0 reading: universalProb_ge_two_pow_neg_prefixComplexity and universalProb_le_one pin P_U(x) to (0, 1]. @audit:ok

Used by