Skip to content

InformationTheory.Shannon.Kolmogorov.Counting

Imports 4

Counting and the existence of incompressible strings #

There are fewer than 2 ^ k natural numbers of complexity below k, because each such x is produced by a program shorter than k bits and the map sending x to its shortest program is injective (a program's output is determined by the program). Since there are only finitely many programs of length below k, only finitely many x can be that simple, and — the type of naturals being infinite — an incompressible x with k ≤ complexity x always exists.

Main statements #

incompressible_count — #{x | complexity x < k} < 2 ^ k.
exists_incompressible — for every k some x has k ≤ complexity x.

def

InformationTheory.Kolmogorov.progNat

:

List Bool → ℕ

Encode a bit string as a positive natural number by reading it as the binary digits below a leading sentinel 1. The sentinel makes the encoding injective (the length is recoverable) and keeps a length-n string below 2 ^ (n + 1).

Equations

InformationTheory.Kolmogorov.progNat [] = 1
InformationTheory.Kolmogorov.progNat (b :: bs) = 2 * InformationTheory.Kolmogorov.progNat bs + b.toNat

Instances For

Used by

theorem

InformationTheory.Kolmogorov.progNat_pos

(p : List Bool) :

Used by

theorem

InformationTheory.Kolmogorov.progNat_lt

(p : List Bool) :

progNat p < 2 ^ (p.length + 1)

Used by

theorem

InformationTheory.Kolmogorov.progNat_injective

:

Function.Injective progNat

Used by

noncomputable def

InformationTheory.Kolmogorov.shortestProg

(x : ℕ) :

A shortest program for x (attained by condComplexity_spec).

Equations

InformationTheory.Kolmogorov.shortestProg x = ⋯.choose

Instances For

Used by

noncomputable def

InformationTheory.Kolmogorov.shortestNat

(x : ℕ) :

The natural-number code of x's shortest program.

Equations

InformationTheory.Kolmogorov.shortestNat x = InformationTheory.Kolmogorov.progNat (InformationTheory.Kolmogorov.shortestProg x)

Instances For

Used by

theorem

InformationTheory.Kolmogorov.shortestProg_length

(x : ℕ) :

(shortestProg x).length = condComplexity x 0

Used by

theorem

InformationTheory.Kolmogorov.shortestProg_mem

(x : ℕ) :

x ∈ universalEval (shortestProg x) 0

Used by

theorem

InformationTheory.Kolmogorov.shortestNat_injective

:

Function.Injective shortestNat

Used by

theorem

InformationTheory.Kolmogorov.shortestNat_lt_of_lt

{x k : ℕ} (hx : complexity x < k) :

shortestNat x < 2 ^ k

Used by

theorem

InformationTheory.Kolmogorov.complexity_lt_finite

(k : ℕ) :

{x : ℕ | complexity x < k}.Finite

Used by

theorem

InformationTheory.Kolmogorov.incompressible_count

(k : ℕ) :

{x : ℕ | complexity x < k}.ncard < 2 ^ k

Fewer than 2 ^ k naturals have complexity below k.

Used by

theorem

InformationTheory.Kolmogorov.exists_incompressible

(k : ℕ) :

∃ (x : ℕ), k ≤ complexity x

For every bound k there is an incompressible x with k ≤ complexity x.

Used by

Conditional version #

The same counting bound holds relative to any condition y, needed for the entropy-rate lower bound where the condition is the block length. The y = 0 declarations above are the unconditional specializations.

noncomputable def

InformationTheory.Kolmogorov.shortestProgCond

(x y : ℕ) :

A shortest program for x under condition y (attained by condComplexity_spec).

Equations

InformationTheory.Kolmogorov.shortestProgCond x y = ⋯.choose

Instances For

Used by

noncomputable def

InformationTheory.Kolmogorov.shortestNatCond

(x y : ℕ) :

The natural-number code of x's shortest program under condition y.

Equations

InformationTheory.Kolmogorov.shortestNatCond x y = InformationTheory.Kolmogorov.progNat (InformationTheory.Kolmogorov.shortestProgCond x y)

Instances For

Used by

theorem

InformationTheory.Kolmogorov.shortestProgCond_length

(x y : ℕ) :

(shortestProgCond x y).length = condComplexity x y

Used by

theorem

InformationTheory.Kolmogorov.shortestProgCond_mem

(x y : ℕ) :

x ∈ universalEval (shortestProgCond x y) y

Used by

theorem

InformationTheory.Kolmogorov.shortestNatCond_injective

(y : ℕ) :

Function.Injective fun (x : ℕ) => shortestNatCond x y

Used by

theorem

InformationTheory.Kolmogorov.shortestNatCond_lt_of_lt

{x y k : ℕ} (hx : condComplexity x y < k) :

shortestNatCond x y < 2 ^ k

Used by

theorem

InformationTheory.Kolmogorov.condComplexity_lt_finite

(y k : ℕ) :

{x : ℕ | condComplexity x y < k}.Finite

Used by

theorem

InformationTheory.Kolmogorov.condIncompressible_count

(y k : ℕ) :

{x : ℕ | condComplexity x y < k}.ncard < 2 ^ k

Fewer than 2 ^ k naturals have conditional complexity below k, for any condition y. @audit:ok

Used by