Skip to content

InformationTheory.Shannon.Kolmogorov.PrefixMachine

Imports 6

A self-delimiting (prefix-free) universal machine for prefix complexity #

The plain universal machine universalEval is not self-delimiting: the echo program false :: encodeNat x is prefix-closed, so its valid-program set is not prefix-free and the Kraft-McMillan inequality does not apply. This file builds a separate machine prefixUniversalEval whose valid-program set is prefix-free.

Every valid program has the shape selfDelimit bs = replicate |bs| true ++ false :: bs (a unary length prefix followed by the payload). The machine reads the unary prefix with parseUnary, accepts only when the recovered length matches the payload length (full self-delimited consumption), and then decodes the payload in the same two modes as the plain machine (literal echo / interpret). Because the accepted set is contained in the prefix-free image of selfDelimit, the Kraft-McMillan inequality applies to each of its finite subsets.

Main definitions #

PrefixFree — a set of bit-string codewords is prefix-free.
selfDelimit — the unary length-prefix self-delimiting wrapper.
prefixUniversalEval — the fixed self-delimiting universal machine.
prefixComplexity — prefix Kolmogorov complexity K(x).
universalProb — the universal probability P_U(x) in ℝ≥0∞.

Main statements #

PrefixFree.uniquelyDecodable — prefix-free (with no empty codeword) implies uniquely decodable, bridging to kraft_mcmillan_inequality.
PrefixFree.kraft / PrefixFree.tsum_inv_two_pow_length_le_one — the finite and infinite Kraft bounds ∑ 2^{-|p|} ≤ 1 for an arbitrary prefix-free set of codewords with no empty codeword.
prefixUniversalEval_kraft — every finite set of valid programs satisfies the Kraft bound ∑ 2^{-|p|} ≤ 1.
tsum_inv_two_pow_length_le_one — the infinite form of the Kraft bound, for any set of valid programs.

def

InformationTheory.Kolmogorov.PrefixFree

(S : Set (List Bool)) :

A set of bit-string codewords is prefix-free (self-delimiting): no codeword is a prefix of a distinct codeword.

Equations

InformationTheory.Kolmogorov.PrefixFree S = ∀ a ∈ S, ∀ b ∈ S, a <+: b → a = b

Instances For

Used by

theorem

InformationTheory.Kolmogorov.PrefixFree.mono

{S S' : Set (List Bool)} (h : PrefixFree S) (hsub : S' ⊆ S) :

Used by

theorem

InformationTheory.Kolmogorov.PrefixFree.uniquelyDecodable

{S : Set (List Bool)} (h : PrefixFree S) (h0 : [] ∉ S) :

UniquelyDecodable S

Prefix-free codes with no empty codeword are uniquely decodable. Not in Mathlib; bridges to kraft_mcmillan_inequality. @audit:ok

Used by

theorem

InformationTheory.Kolmogorov.uniquelyDecodable_mono

{S S' : Set (List Bool)} (h : UniquelyDecodable S) (hsub : S' ⊆ S) :

UniquelyDecodable S'

Used by

def

InformationTheory.Kolmogorov.selfDelimit

(bs : List Bool) :

The unary length-prefix self-delimiting wrapper: bs.length in unary (a run of trues terminated by false) followed by the payload bs. Its image over all payloads is prefix-free.

Equations

InformationTheory.Kolmogorov.selfDelimit bs = List.replicate bs.length true ++ false :: bs

Instances For

Used by

theorem

InformationTheory.Kolmogorov.parseUnary_snd_eq_nil_of_not_mem

{p : List Bool} (h : false ∉ p) :

(parseUnary p).2 = []

Used by

theorem

InformationTheory.Kolmogorov.parseUnary_reconstruct

{p : List Bool} (h : false ∈ p) :

p = List.replicate (parseUnary p).1 true ++ false :: (parseUnary p).2

Used by

theorem

InformationTheory.Kolmogorov.parseUnary_selfDelimit

(bs : List Bool) :

parseUnary (selfDelimit bs) = (bs.length, bs)

Used by

theorem

InformationTheory.Kolmogorov.selfDelimit_length

(bs : List Bool) :

(selfDelimit bs).length = 2 * bs.length + 1

Used by

theorem

InformationTheory.Kolmogorov.range_selfDelimit_prefixFree

:

PrefixFree (Set.range selfDelimit)

Used by

noncomputable def

InformationTheory.Kolmogorov.decodePayload

:

List Bool → Part ℕ

Decode a self-delimited payload. false :: bs echoes decodeNat bs; true :: bs interprets bs as a code index (unary) plus a description, delegating to Mathlib's universal interpreter eval.

Equations

One or more equations did not get rendered due to their size.
InformationTheory.Kolmogorov.decodePayload [] = Part.none
InformationTheory.Kolmogorov.decodePayload (false :: bs) = Part.some (Computability.decodeNat bs)

Instances For

Used by

noncomputable def

InformationTheory.Kolmogorov.prefixUniversalEval

(p : List Bool) :

The fixed self-delimiting universal machine. A program is accepted only if its unary length prefix matches the payload length (so its domain lies in the prefix-free image of selfDelimit), then the payload is decoded.

Equations

One or more equations did not get rendered due to their size.

Instances For

Used by

theorem

InformationTheory.Kolmogorov.decodePayload_dom_ne_nil

{q : List Bool} (h : (decodePayload q).Dom) :

Used by

theorem

InformationTheory.Kolmogorov.prefixUniversalEval_nil_not_dom

:

¬(prefixUniversalEval []).Dom

Used by

theorem

InformationTheory.Kolmogorov.dom_imp_mem_range

{p : List Bool} (h : (prefixUniversalEval p).Dom) :

p ∈ Set.range selfDelimit

Used by

theorem

InformationTheory.Kolmogorov.prefixUniversalEval_dom_prefixFree

:

PrefixFree {p : List Bool | (prefixUniversalEval p).Dom}

Used by

def

InformationTheory.Kolmogorov.prefixLiteralProg

(x : ℕ) :

The prefix echo program describing x: x's binary payload wrapped by the literal mode flag and the self-delimiting length prefix.

Equations

InformationTheory.Kolmogorov.prefixLiteralProg x = InformationTheory.Kolmogorov.selfDelimit (false :: Computability.encodeNat x)

Instances For

Used by

theorem

InformationTheory.Kolmogorov.prefixUniversalEval_literal

(x : ℕ) :

prefixUniversalEval (prefixLiteralProg x) = Part.some x

Used by

theorem

InformationTheory.Kolmogorov.PrefixFree.kraft

{S : Set (List Bool)} (hS : PrefixFree S) (h0 : [] ∉ S) (u : Finset (List Bool)) (hu : ↑u ⊆ S) :

∑ p ∈ u, (1 / 2) ^ p.length ≤ 1

The Kraft-McMillan bound ∑ 2^{-|p|} ≤ 1 for a finite subset of an arbitrary prefix-free set of codewords with no empty codeword. @audit:ok

Used by

theorem

InformationTheory.Kolmogorov.prefixUniversalEval_kraft

(u : Finset (List Bool)) (hu : ∀ p ∈ u, (prefixUniversalEval p).Dom) :

∑ p ∈ u, (1 / 2) ^ p.length ≤ 1

Every finite set of valid programs of the self-delimiting machine satisfies the Kraft-McMillan bound ∑ 2^{-|p|} ≤ 1. @audit:ok

Used by

theorem

InformationTheory.Kolmogorov.PrefixFree.tsum_inv_two_pow_length_le_one

{S : Set (List Bool)} (hS : PrefixFree S) (h0 : [] ∉ S) :

∑' (p : { p : List Bool // p ∈ S }), 2⁻¹ ^ (↑p).length ≤ 1

The infinite Kraft bound for an arbitrary prefix-free set of codewords: the total weight ∑ 2^{-|p|} is at most 1. Every finite subsum is a Kraft sum, and ℝ≥0∞-valued sums are suprema of those. @audit:ok

Used by

theorem

InformationTheory.Kolmogorov.tsum_inv_two_pow_length_le_one

{P : List Bool → Prop} (hP : ∀ (p : List Bool), P p → (prefixUniversalEval p).Dom) :

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

The infinite Kraft bound: any set of valid programs of the self-delimiting machine, cut out by a predicate P, has total weight ∑ 2^{-|p|} ≤ 1. This is PrefixFree.tsum_inv_two_pow_length_le_one specialized to the machine's domain, which is prefix-free and contains no empty codeword. @audit:ok

Used by

noncomputable def

InformationTheory.Kolmogorov.prefixComplexity

(x : ℕ) :

Prefix Kolmogorov complexity K(x): the length of the shortest self-delimiting program producing x. The literal echo makes the set nonempty, so this infimum is attained (prefixComplexity_spec).

Equations

InformationTheory.Kolmogorov.prefixComplexity x = sInf {l : ℕ | ∃ (p : List Bool), p.length = l ∧ x ∈ InformationTheory.Kolmogorov.prefixUniversalEval p}

Instances For

Used by

theorem

InformationTheory.Kolmogorov.prefixComplexity_set_nonempty

(x : ℕ) :

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

Used by

theorem

InformationTheory.Kolmogorov.prefixComplexity_spec

(x : ℕ) :

∃ (p : List Bool), p.length = prefixComplexity x ∧ x ∈ prefixUniversalEval p

Used by

noncomputable def

InformationTheory.Kolmogorov.universalProb

(x : ℕ) :

Universal probability P_U(x) = ∑_{p : U_prefix p = x} 2^{-|p|} in ℝ≥0∞. The tsum is always defined; P_U(x) ≤ 1 follows from Kraft on finite subsets.

Equations

InformationTheory.Kolmogorov.universalProb x = ∑' (p : { p : List Bool // x ∈ InformationTheory.Kolmogorov.prefixUniversalEval p }), 2⁻¹ ^ (↑p).length

Instances For

Used by