InformationTheory.Shannon.Kolmogorov.UniversalProbability

Imports 4

The universal probability of a natural number #

Cover–Thomas (2nd ed.). The universal probability universalProb x is the total weight ∑ 2^{-|p|} of the self-delimiting programs p that output x. Since the shortest such program has length prefixComplexity x, its single term already gives the lower bound 2^{-K(x)} ≤ P_U(x), while the Kraft bound on the self-delimiting machine gives P_U(x) ≤ 1 on every finite subsum.

Together the two bounds place P_U(x) in the interval (0, 1], so its real logarithm is well defined and -log₂ P_U(x) ≤ K(x) — one half of Levin's coding theorem.

Main statements #

universalProb_ge_two_pow_neg_prefixComplexity — the lower bound 2^{-K(x)} ≤ P_U(x).
universalProb_le_one — the Kraft bound P_U(x) ≤ 1.
neg_logb_universalProb_le_prefixComplexity — the logarithmic form -log₂ P_U(x) ≤ K(x).

theorem

InformationTheory.Kolmogorov.universalProb_ge_two_pow_neg_prefixComplexity

source

(x : ℕ) :

2⁻¹ ^ prefixComplexity x ≤ universalProb x

The universal probability dominates the weight of a shortest program: 2^{-K(x)} ≤ P_U(x). @audit:ok

Used by

theorem

InformationTheory.Kolmogorov.universalProb_le_one

source

(x : ℕ) :

universalProb x ≤ 1

The universal probability is a subprobability: P_U(x) ≤ 1, because every finite subsum is a Kraft sum of valid self-delimiting programs. @audit:ok

Used by

theorem

InformationTheory.Kolmogorov.neg_logb_universalProb_le_prefixComplexity

source

(x : ℕ) :

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

The logarithmic form of the lower bound: -log₂ P_U(x) ≤ K(x), one half of Levin's coding theorem. 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