InformationTheory.Shannon.Kolmogorov.Incompressible

Imports 5

Incompressible binary sequences obey the law of large numbers #

Cover–Thomas (2nd ed.). An incompressible length-n binary string — one whose conditional Kolmogorov complexity is at least its own length, n ≤ C(encodeBlock n b ∣ n) — has empirical frequency of ones typeCount b true / n close to 1/2, and for a family of such strings the frequency converges to 1/2 as n → ∞.

The argument is purely combinatorial (measure-free): it reuses the method-of-types per-string upper bound of EntropyRate.lean with its typicality step removed, so that the empirical binary entropy binEntropy (typeCount b true / n) bounds the description length. Incompressibility then forces the binary entropy up to its maximum log 2, and strict unimodality of binEntropy (via a fixed positive gap away from 1/2) pins the frequency to 1/2.

Main statements #

incompressible_freq_near_half — the frequency of ones of every incompressible block is eventually within any δ > 0 of 1/2.
incompressible_seq_freq_tendsto_half — along an eventually-incompressible family, the frequency of ones converges to 1/2.

theorem

InformationTheory.Kolmogorov.entropyByCount_bool_eq_binEntropy

source

{n : ℕ} (hn : 0 < n) (b : Fin n → Bool) :

Shannon.entropyByCount (Shannon.typeCount b) n = Real.binEntropy (↑(Shannon.typeCount b true) / ↑n)

On the two-element alphabet the empirical entropy of a block's type equals the binary entropy of its frequency of ones. @audit:ok

Used by

theorem

InformationTheory.Kolmogorov.condComplexity_bool_block_le

source

∃ (c : ℝ), 0 ≤ c ∧ ∀ {n : ℕ}, 0 < n → ∀ (b : Fin n → Bool), ↑(condComplexity (encodeBlock n b) n) ≤ 2 * Real.logb 2 (↑n + 1) + ↑n * (Real.binEntropy (↑(Shannon.typeCount b true) / ↑n) / Real.log 2) + c

Raw per-string upper bound (measure-free): the conditional complexity of a binary block is bounded by the type-descriptor overhead plus n · binEntropy(p)/log 2, with p the frequency of ones. Obtained from condComplexity_block_typical_le by dropping the typicality step. @audit:ok

Used by

theorem

InformationTheory.Kolmogorov.binEntropy_gap_of_far_from_half

source

{p δ : ℝ} (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (hδ0 : 0 < δ) (hδ1 : δ ≤ 2⁻¹) (hfar : δ ≤ |p - 2⁻¹ |) :

Real.binEntropy p ≤ Real.binEntropy (2⁻¹ - δ)

Fixed-gap analytic core: if the frequency p is at least δ away from 1/2, then its binary entropy is at most binEntropy (1/2 - δ), which is strictly below log 2. @audit:ok

Used by

theorem

InformationTheory.Kolmogorov.exists_incompressible_bool_seq

source

∃ (w : (n : ℕ) → Fin n → Bool), ∀ (n : ℕ), 0 < n → ↑n ≤ ↑(condComplexity (encodeBlock n (w n)) n)

Incompressible binary blocks exist at every length: since fewer than 2^n naturals have conditional complexity below n, some length-n block is incompressible. @audit:ok

Used by

theorem

InformationTheory.Kolmogorov.incompressible_freq_near_half

source

{δ : ℝ} (hδ : 0 < δ) :

∀ᶠ (n : ℕ) in Filter.atTop , ∀ (b : Fin n → Bool), ↑n ≤ ↑(condComplexity (encodeBlock n b) n) → |↑(Shannon.typeCount b true) / ↑n - 2⁻¹ | < δ

CT 14.5.1: the frequency of ones of every incompressible binary block is eventually within δ of 1/2. @audit:ok

Used by

theorem

InformationTheory.Kolmogorov.incompressible_seq_freq_tendsto_half

source

(w : (n : ℕ) → Fin n → Bool) (hw : ∀ᶠ (n : ℕ) in Filter.atTop , ↑n ≤ ↑(condComplexity (encodeBlock n (w n)) n)) :

Filter.Tendsto (fun (n : ℕ) => ↑(Shannon.typeCount (w n) true) / ↑n) Filter.atTop (nhds 2⁻¹)

Law-of-large-numbers corollary: along an eventually-incompressible family the frequency of ones converges to 1/2. @audit:ok

Used by