Skip to content

InformationTheory.Shannon.Kolmogorov.EntropyRate

Imports 11

Kolmogorov complexity converges to the entropy rate #

For an i.i.d. source Xs on a finite alphabet, the expected conditional Kolmogorov complexity of a length-n block, normalized by n, converges to the entropy H(X) re-based to bits:

(1 / n) · E[C(X^n ∣ n)] → H(X) / log 2.

The / log 2 re-bases the natural-log entropy entropy (Bridge.lean, base e) to the bit-length complexity condComplexity (base 2).

The proof is a squeeze between an upper and a lower half. The upper half encodes a typical block by its index inside the typical set (bits ≈ n(H+ε)) on top of the conditional literal bound; the lower half combines the counting bound #{x ∣ C(x ∣ n) < k} < 2^k with the strong-typicality size lower bound. This file establishes the flagship statement and the plumbing lemmas the two halves consume.

Main definitions #

encodeBlock — the base-card α numeral encoding a length-m block as ℕ.

Main statements #

kolmogorov_entropy_rate — the flagship convergence (via the two halves).
encodeBlock_injective — that encoding of a block as ℕ is injective.
integrable_condComplexity_jointRV — the block-complexity integrand is integrable.

theorem

InformationTheory.Kolmogorov.ofDigits_ofFn

(b : ℕ) {m : ℕ} (f : Fin m → ℕ) :

Nat.ofDigits b (List.ofFn f) = ∑ i : Fin m, f i * b ^ ↑i

Used by

noncomputable def

InformationTheory.Kolmogorov.encodeBlock

{α : Type u_1} [Fintype α] (m : ℕ) (x : Fin m → α) :

Injective, length-efficient encoding of a length-m block Fin m → α into a natural number: the little-endian base-Fintype.card α numeral whose i-th digit is the index of x i under Fintype.equivFin. Its value is below card α ^ m, so its bit length is m · log₂ (card α) + O(1).

Equations

InformationTheory.Kolmogorov.encodeBlock m x = ↑(finFunctionFinEquiv fun (i : Fin m) => (Fintype.equivFin α) (x i))

Instances For

Used by

theorem

InformationTheory.Kolmogorov.encodeBlock_injective

{α : Type u_1} [Fintype α] (m : ℕ) :

Function.Injective (encodeBlock m)

Used by

theorem

InformationTheory.Kolmogorov.encodeBlock_lt

{α : Type u_1} [Fintype α] (m : ℕ) (x : Fin m → α) :

encodeBlock m x < Fintype.card α ^ m

Used by

theorem

InformationTheory.Kolmogorov.encodeBlock_eq_ofDigits

{α : Type u_1} [Fintype α] (m : ℕ) (x : Fin m → α) :

encodeBlock m x = Nat.ofDigits (Fintype.card α) (List.ofFn fun (i : Fin m) => ↑((Fintype.equivFin α) (x i)))

Used by

Base-conversion bridges (bit length `2^k` ↔ natural-log `exp`) #

theorem

InformationTheory.Kolmogorov.log_two_pos

:

Used by

theorem

InformationTheory.Kolmogorov.two_pow_eq_exp

(k : ℕ) :

2 ^ k = Real.exp (↑k * Real.log 2)

Used by

theorem

InformationTheory.Kolmogorov.exp_le_two_pow_iff

(t : ℝ) (k : ℕ) :

Real.exp t ≤ 2 ^ k ↔ t ≤ ↑k * Real.log 2

Used by

Type-class decoder matching (upper-bound crux) #

The upper half feeds the type-class decoder typeDecoder (EntropyRateUpper.lean) to invariance. The matching lemmas below connect the block encoder encodeBlock to typeDecoder, and bound the index range by the type-class cardinality.

theorem

InformationTheory.Kolmogorov.ofDigits_inj

{b : ℕ} (hb : 0 < b) (L1 L2 : List ℕ) (hlen : L1.length = L2.length) (h1 : ∀ d ∈ L1, d < b) (h2 : ∀ d ∈ L2, d < b) (heq : Nat.ofDigits b L1 = Nat.ofDigits b L2) :

L1 = L2

Base-b numerals of equal length with all digits below b are determined by their value: Nat.ofDigits is injective on such digit lists.

Used by

The entropy-rate theorem #

theorem

InformationTheory.Kolmogorov.integrable_condComplexity_jointRV

{α : Type u_1} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] {Ω : Type u_2} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (Xs : ℕ → Ω → α) (hXs : ∀ (i : ℕ), Measurable (Xs i)) (n : ℕ) :

MeasureTheory.Integrable (fun (ω : Ω) => ↑(condComplexity (encodeBlock n (Shannon.jointRV Xs n ω)) n)) μ

The block-complexity integrand takes finitely many values (the block space is finite), so it is a bounded measurable function and hence integrable. @audit:ok

Used by

theorem

InformationTheory.Kolmogorov.mem_decoderAlphabet

{α : Type u_1} [Fintype α] (a : α) :

a ∈ decoderAlphabet

Used by

theorem

InformationTheory.Kolmogorov.length_decoderAlphabet

{α : Type u_1} [Fintype α] :

decoderAlphabet.length = Fintype.card α

Used by

theorem

InformationTheory.Kolmogorov.enumWords_succ

{α : Type u_1} [Fintype α] (n : ℕ) :

enumWords (n + 1) = List.flatMap (fun (w : List α) => List.map (fun (a : α) => a :: w) decoderAlphabet) (enumWords n)

Used by

theorem

InformationTheory.Kolmogorov.mem_enumWords_iff

{α : Type u_1} [Fintype α] (n : ℕ) (w : List α) :

w ∈ enumWords n ↔ w.length = n

Used by

theorem

InformationTheory.Kolmogorov.enumWords_nodup

{α : Type u_1} [Fintype α] (n : ℕ) :

(enumWords n).Nodup

Used by

theorem

InformationTheory.Kolmogorov.length_typeSig

{α : Type u_1} [Fintype α] [DecidableEq α] (w : List α) :

(typeSig w).length = Fintype.card α

Used by

theorem

InformationTheory.Kolmogorov.typeSig_lt

{α : Type u_1} [Fintype α] [DecidableEq α] {n : ℕ} {w : List α} (hw : w.length = n) (d : ℕ) :

d ∈ typeSig w → d < n + 1

Used by

theorem

InformationTheory.Kolmogorov.typeCode_lt

{α : Type u_1} [Fintype α] [DecidableEq α] {n : ℕ} (hn : 0 < n) {w : List α} (hw : w.length = n) :

Nat.ofDigits (n + 1) (typeSig w) < (n + 1) ^ Fintype.card α

The base-(n+1) numeral of a length-n signature is below K = (n+1) ^ card α.

Used by

theorem

InformationTheory.Kolmogorov.typeCount_filter_ofFn

{α : Type u_1} [DecidableEq α] {n : ℕ} (x : Fin n → α) (a : α) :

(List.filter (fun (c : α) => decide (c = a)) (List.ofFn x)).length = Shannon.typeCount x a

Used by

theorem

InformationTheory.Kolmogorov.typeSig_ofFn

{α : Type u_1} [Fintype α] [DecidableEq α] {n : ℕ} (x : Fin n → α) :

typeSig (List.ofFn x) = List.map (fun (a : α) => Shannon.typeCount x a) decoderAlphabet

Used by

noncomputable def

InformationTheory.Kolmogorov.toBlock

{α : Type u_1} [Nonempty α] (n : ℕ) (w : List α) :

Fin n → α

A partial inverse of List.ofFn: reconstruct a block from a length-n word.

Equations

InformationTheory.Kolmogorov.toBlock n w i = w.getD (↑i) (Classical.arbitrary α)

Instances For

Used by

theorem

InformationTheory.Kolmogorov.ofFn_toBlock

{α : Type u_1} [Nonempty α] {n : ℕ} {w : List α} (hw : w.length = n) :

List.ofFn (toBlock n w) = w

Used by

theorem

InformationTheory.Kolmogorov.filter_typeSig_length_le

{α : Type u_1} [Fintype α] [DecidableEq α] [Nonempty α] {n : ℕ} (hn : 0 < n) (b : Fin n → α) :

(List.filter (fun (w : List α) => decide (Nat.ofDigits (n + 1) (typeSig w) = Nat.ofDigits (n + 1) (typeSig (List.ofFn b)))) (enumWords n)).length ≤ ⋯.toFinset.card

The words sharing a block's signature are no more numerous than its type class.

Used by

theorem

InformationTheory.Kolmogorov.exists_mem_typeDecoder_lt

{α : Type u_1} [Fintype α] [DecidableEq α] [Nonempty α] {n : ℕ} (hn : 0 < n) (b : Fin n → α) :

∃ (m : ℕ), encodeBlock n b ∈ typeDecoder m n ∧ m < (n + 1) ^ Fintype.card α * ⋯.toFinset.card

The block encoder is matched by the type-class decoder at an index below the packed bound K · |T_c|: there is a program number m decoding to encodeBlock n b whose value is below (n+1) ^ card α times the type-class cardinality.

Used by

theorem

InformationTheory.Kolmogorov.framing_overhead_eventually

(c₀ D : ℝ) {δ : ℝ} (hδ : 0 < δ) :

∀ᶠ (n : ℕ) in Filter.atTop , c₀ + D * Real.logb 2 (↑n + 1) ≤ ↑n * δ

The O(log n) framing overhead is eventually dominated by any positive linear slack n · δ, since logb 2 (n + 1) = o(n).

Used by

theorem

InformationTheory.Kolmogorov.entropyByCount_le_of_strongTypical

{α : Type u_1} [Fintype α] [DecidableEq α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] {Ω : Type u_2} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (Xs : ℕ → Ω → α) (hXs : ∀ (i : ℕ), Measurable (Xs i)) {n : ℕ} (hn : 0 < n) {ε : ℝ} (x : Fin n → α) (hx : x ∈ Shannon.stronglyTypicalSet μ Xs n ε) (hpos : ∀ (a : α), 0 < (MeasureTheory.Measure.map (Xs 0) μ).real {a}) :

Shannon.entropyByCount (Shannon.typeCount x) n ≤ Shannon.entropy μ (Xs 0) + ε * Shannon.logSumAbs μ Xs

On the strongly-typical set, the empirical entropy of a block's type is bounded above by the true entropy plus the linear typicality slack ε · L.

Used by

theorem

InformationTheory.Kolmogorov.condComplexity_block_typical_le

{α : Type u_1} [Fintype α] [DecidableEq α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] {Ω : Type u_2} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (Xs : ℕ → Ω → α) (hXs : ∀ (i : ℕ), Measurable (Xs i)) (hpos : ∀ (a : α), 0 < (MeasureTheory.Measure.map (Xs 0) μ).real {a}) {ε : ℝ} (hε : 0 < ε) {δ : ℝ} (hδ : 0 < δ) :

∀ᶠ (n : ℕ) in Filter.atTop , ∀ b ∈ Shannon.stronglyTypicalSet μ Xs n ε, ↑(condComplexity (encodeBlock n b) n) ≤ ↑n * ((Shannon.entropy μ (Xs 0) + ε * Shannon.logSumAbs μ Xs) / Real.log 2) + ↑n * δ

Per-string upper bound on the strongly typical set (method of types): a typical block is described by its type descriptor together with its index inside the type class, costing n · (H + ε·L)/log 2 + o(n) bits. The o(n) overhead (the type descriptor |α|·log n and the pairing/framing constant) is absorbed as an arbitrarily small linear slack n · δ, valid for all large n. @audit:ok

Used by

theorem

InformationTheory.Kolmogorov.condComplexity_block_uniform_le

{α : Type u_1} [Fintype α] :

∃ (C : ℝ), 0 ≤ C ∧ ∀ (n : ℕ) (b : Fin n → α), ↑(condComplexity (encodeBlock n b) n) ≤ C * (↑n + 1)

Uniform per-string upper bound: every length-n block is describable by echoing its base-card α numeral, costing natLen ≤ n · ⌈log₂ card α⌉ bits plus the literal flag, so C(x | n) ≤ (⌈log₂ card α⌉ + 1) · (n + 1). @audit:ok

Used by

theorem

InformationTheory.Kolmogorov.kolmogorov_entropy_rate_upper

{α : Type u_1} [Fintype α] [DecidableEq α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] {Ω : Type u_2} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (Xs : ℕ → Ω → α) (hXs : ∀ (i : ℕ), Measurable (Xs i)) (_hindep_full : ProbabilityTheory.iIndepFun (fun (i : ℕ) => Xs i) μ) (hindep_pair : Pairwise fun (i j : ℕ) => ProbabilityTheory.IndepFun (Xs i) (Xs j) μ) (hident : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (Xs i) (Xs 0) μ μ) (hpos : ∀ (a : α), 0 < (MeasureTheory.Measure.map (Xs 0) μ).real {a}) (ε : ℝ) :

0 < ε → ∀ᶠ (n : ℕ) in Filter.atTop , 1 / ↑n * ∫ (ω : Ω), ↑(condComplexity (encodeBlock n (Shannon.jointRV Xs n ω)) n) ∂μ ≤ Shannon.entropy μ (Xs 0) / Real.log 2 + ε

Upper half: eventually the normalized expected complexity is within ε above H / log 2. Method-of-types assembly: split the integral at the strongly typical set, bound the typical part by condComplexity_block_typical_le and the atypical part by condComplexity_block_uniform_le, then let the atypical mass vanish. The assembly itself is unconditional, resting only on the two per-string bounds above.

Used by

Lower-half building blocks #

theorem

InformationTheory.Kolmogorov.blockLaw_eq_pi

{α : Type u_1} [MeasurableSpace α] {Ω : Type u_2} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (Xs : ℕ → Ω → α) (hXs : ∀ (i : ℕ), Measurable (Xs i)) (hindep_full : ProbabilityTheory.iIndepFun (fun (i : ℕ) => Xs i) μ) (hident : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (Xs i) (Xs 0) μ μ) (n : ℕ) :

MeasureTheory.Measure.map (Shannon.jointRV Xs n) μ = MeasureTheory.Measure.pi fun (x : Fin n) => MeasureTheory.Measure.map (Xs 0) μ

The block law of an i.i.d. source is the product measure of the marginal. @audit:ok

Used by

theorem

InformationTheory.Kolmogorov.blockProb_eq_prod

{α : Type u_1} [MeasurableSpace α] {Ω : Type u_2} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (Xs : ℕ → Ω → α) (hXs : ∀ (i : ℕ), Measurable (Xs i)) (hindep_full : ProbabilityTheory.iIndepFun (fun (i : ℕ) => Xs i) μ) (hident : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (Xs i) (Xs 0) μ μ) (n : ℕ) (b : Fin n → α) :

(MeasureTheory.Measure.map (Shannon.jointRV Xs n) μ).real {b} = ∏ i : Fin n, (MeasureTheory.Measure.map (Xs 0) μ).real {b i}

The probability of a single block factors over the coordinates. @audit:ok

Used by

theorem

InformationTheory.Kolmogorov.typicalSet_blockProb_le

{α : Type u_1} [Fintype α] [MeasurableSpace α] {Ω : Type u_2} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (Xs : ℕ → Ω → α) (hpos : ∀ (a : α), 0 < (MeasureTheory.Measure.map (Xs 0) μ).real {a}) (n : ℕ) {ε : ℝ} (b : Fin n → α) (hb : b ∈ Shannon.typicalSet μ Xs n ε) :

∏ i : Fin n, (MeasureTheory.Measure.map (Xs 0) μ).real {b i} ≤ Real.exp (-(↑n * (Shannon.entropy μ (Xs 0) - ε)))

A typical block has product mass at most exp (-n (H - ε)) (the mirror of the typicalSet_card_le lower bound). @audit:ok

Used by

theorem

InformationTheory.Kolmogorov.compressibleBlocks_card_lt

{α : Type u_1} [Fintype α] (n k : ℕ) :

↑{b : Fin n → α | condComplexity (encodeBlock n b) n < k}.ncard < 2 ^ k

Fewer than 2 ^ k blocks have conditional complexity below k, via the injective block encoding and the counting bound condIncompressible_count. @audit:ok

Used by

theorem

InformationTheory.Kolmogorov.compressible_prob_le

{α : Type u_1} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] {Ω : Type u_2} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (Xs : ℕ → Ω → α) (hXs : ∀ (i : ℕ), Measurable (Xs i)) (hindep_full : ProbabilityTheory.iIndepFun (fun (i : ℕ) => Xs i) μ) (hident : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (Xs i) (Xs 0) μ μ) (hpos : ∀ (a : α), 0 < (MeasureTheory.Measure.map (Xs 0) μ).real {a}) (n k : ℕ) {ε₁ : ℝ} :

μ.real {ω : Ω | Shannon.jointRV Xs n ω ∈ Shannon.typicalSet μ Xs n ε₁ ∧ condComplexity (encodeBlock n (Shannon.jointRV Xs n ω)) n < k} ≤ 2 ^ k * Real.exp (-(↑n * (Shannon.entropy μ (Xs 0) - ε₁)))

The mass of the typical-and-compressible blocks is at most 2 ^ k · exp (-n (H - ε₁)) (product bound times a count below 2 ^ k). @audit:ok

Used by

theorem

InformationTheory.Kolmogorov.floor_mul_div_tendsto

(c : ℝ) (hc : 0 ≤ c) :

Filter.Tendsto (fun (n : ℕ) => ↑⌊↑n * c⌋₊ / ↑n) Filter.atTop (nhds c)

The floor ⌊n c⌋₊, normalized by n, converges to c (for c ≥ 0). @audit:ok

Used by

theorem

InformationTheory.Kolmogorov.kolmogorov_entropy_rate_lower

{α : Type u_1} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] {Ω : Type u_2} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (Xs : ℕ → Ω → α) (hXs : ∀ (i : ℕ), Measurable (Xs i)) (hindep_full : ProbabilityTheory.iIndepFun (fun (i : ℕ) => Xs i) μ) (hindep_pair : Pairwise fun (i j : ℕ) => ProbabilityTheory.IndepFun (Xs i) (Xs j) μ) (hident : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (Xs i) (Xs 0) μ μ) (hpos : ∀ (a : α), 0 < (MeasureTheory.Measure.map (Xs 0) μ).real {a}) (ε : ℝ) :

0 < ε → ∀ᶠ (n : ℕ) in Filter.atTop , Shannon.entropy μ (Xs 0) / Real.log 2 - ε ≤ 1 / ↑n * ∫ (ω : Ω), ↑(condComplexity (encodeBlock n (Shannon.jointRV Xs n ω)) n) ∂μ

Lower half: eventually the normalized expected complexity is within ε below H / log 2. The counting bound condIncompressible_count caps how many blocks can be compressed below k, while the strong-typicality mass spreads over ≈ exp (nH) blocks; a Markov step then pushes the average up to H / log 2 - ε. @audit:ok

Used by

theorem

InformationTheory.Kolmogorov.kolmogorov_entropy_rate

{α : Type u_1} [Fintype α] [DecidableEq α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] {Ω : Type u_2} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] (Xs : ℕ → Ω → α) (hXs : ∀ (i : ℕ), Measurable (Xs i)) (hindep_full : ProbabilityTheory.iIndepFun (fun (i : ℕ) => Xs i) μ) (hindep_pair : Pairwise fun (i j : ℕ) => ProbabilityTheory.IndepFun (Xs i) (Xs j) μ) (hident : ∀ (i : ℕ), ProbabilityTheory.IdentDistrib (Xs i) (Xs 0) μ μ) (hpos : ∀ (a : α), 0 < (MeasureTheory.Measure.map (Xs 0) μ).real {a}) :

Filter.Tendsto (fun (n : ℕ) => 1 / ↑n * ∫ (ω : Ω), ↑(condComplexity (encodeBlock n (Shannon.jointRV Xs n ω)) n) ∂μ) Filter.atTop (nhds (Shannon.entropy μ (Xs 0) / Real.log 2))

Kolmogorov complexity converges to the entropy rate: for an i.i.d. source, the normalized expected conditional complexity of a length-n block tends to the bit-rebased entropy H(X) / log 2 (CT 2nd ed.). @audit:ok

Used by