Incompressibility

There are only 2 ^ r - 1 binary programs of length below r, and each describes at most one object. So, for every description method, fewer than 2 ^ r objects have complexity below r, whatever the time bound. Counting strings of length n then shows that some string of every length n has complexity at least n, and that fewer than a 2 ^ (-c) fraction of the strings of length n have complexity below n - c Li and Vitányi, Chapter 2, Sipser, Section 6.4.

Main results

• Cslib.Kolmogorov.DescriptionMethod.encard_setOf_ecomplexity_lt, Cslib.Kolmogorov.DescriptionMethod.encard_setOf_etimeBoundedComplexity_lt: fewer than 2 ^ r objects have (time-bounded) complexity below r.
• Cslib.Kolmogorov.DescriptionMethod.exists_mem_le_ecomplexity: a set of at least 2 ^ r objects has an element of complexity at least r.
• Cslib.Kolmogorov.DescriptionMethod.ncard_lt_ncard_setOf_le_ecomplexity_add: all but fewer than 2 ^ r elements of a finite set have complexity at least r.
• Cslib.Kolmogorov.DescriptionMethod.exists_length_eq_forall_le_etimeBoundedComplexity: for every n some string of length n has complexity at least n under every time bound.
• Cslib.Kolmogorov.DescriptionMethod.encard_setOf_length_eq_ecomplexity_lt, Cslib.Kolmogorov.DescriptionMethod.two_pow_lt_ncard_setOf_length_eq_le_ecomplexity_add: fewer than 2 ^ (n - c) strings of length n have complexity below n - c.

References

• M. Li, P. Vitányi, An Introduction to Kolmogorov Complexity and Its Applications
• M. Sipser, Introduction to the Theory of Computation

Few objects have low complexity

theorem Cslib.Kolmogorov.DescriptionMethod.encard_setOf_ecomplexity_lt {α : Type u_1} (M : DescriptionMethod α) (r : ℕ) : {x : α | M.ecomplexity x < ↑r}.encard < 2 ^ r

Incompressibility. Fewer than 2 ^ r objects have complexity below r: they have distinct shortest programs, all of length below r.

theorem Cslib.Kolmogorov.DescriptionMethod.encard_setOf_etimeBoundedComplexity_lt {α : Type u_1} (M : DescriptionMethod α) (t r : ℕ) : {x : α | M.etimeBoundedComplexity t x < ↑r}.encard < 2 ^ r

Fewer than 2 ^ r objects have time-bounded complexity below r, for every time bound.

theorem Cslib.Kolmogorov.DescriptionMethod.exists_mem_le_ecomplexity {α : Type u_1} (M : DescriptionMethod α) {s : Set α} {r : ℕ} (hs : 2 ^ r ≤ s.encard) : ∃ x ∈ s, ↑r ≤ M.ecomplexity x

A set of at least 2 ^ r objects has an element of complexity at least r.

theorem Cslib.Kolmogorov.DescriptionMethod.ncard_lt_ncard_setOf_le_ecomplexity_add {α : Type u_1} (M : DescriptionMethod α) {s : Set α} (hs : s.Finite) (r : ℕ) : s.ncard < {x : α | x ∈ s ∧ ↑r ≤ M.ecomplexity x}.ncard + 2 ^ r

All but fewer than 2 ^ r elements of a finite set have complexity at least r.

Incompressible strings

theorem Cslib.Kolmogorov.DescriptionMethod.exists_length_eq_le_ecomplexity (M : DescriptionMethod (List Bool)) (n : ℕ) : ∃ (x : List Bool), x.length = n ∧ ↑n ≤ M.ecomplexity x

Incompressible strings exist. For every n, some string of length n has complexity at least n.

theorem Cslib.Kolmogorov.DescriptionMethod.exists_length_eq_forall_le_etimeBoundedComplexity (M : DescriptionMethod (List Bool)) (n : ℕ) : ∃ (x : List Bool), x.length = n ∧ ∀ (t : ℕ), ↑n ≤ M.etimeBoundedComplexity t x

For every n, some string of length n has complexity at least n under every time bound.

theorem Cslib.Kolmogorov.DescriptionMethod.encard_setOf_length_eq_ecomplexity_lt (M : DescriptionMethod (List Bool)) (n c : ℕ) : {x : List Bool | x.length = n ∧ M.ecomplexity x < ↑(n - c)}.encard < 2 ^ (n - c)

Most strings are nearly incompressible. Fewer than 2 ^ (n - c) strings of length n have complexity below n - c.

theorem Cslib.Kolmogorov.DescriptionMethod.encard_setOf_length_eq_etimeBoundedComplexity_lt (M : DescriptionMethod (List Bool)) (t n c : ℕ) : {x : List Bool | x.length = n ∧ M.etimeBoundedComplexity t x < ↑(n - c)}.encard < 2 ^ (n - c)

Fewer than 2 ^ (n - c) strings of length n have time-bounded complexity below n - c.

theorem Cslib.Kolmogorov.DescriptionMethod.two_pow_lt_ncard_setOf_length_eq_le_ecomplexity_add (M : DescriptionMethod (List Bool)) (n c : ℕ) : 2 ^ n < {x : List Bool | x.length = n ∧ ↑(n - c) ≤ M.ecomplexity x}.ncard + 2 ^ (n - c)

All but fewer than 2 ^ (n - c) of the 2 ^ n strings of length n have complexity at least n - c.