InformationTheory.Shannon.ShannonCode.Basic

Imports 6

Shannon code (per-symbol prefix code achievability) #

For a probability distribution P on a finite alphabet α, the Shannon codeword length l(a) := ⌈−logb D P(a)⌉₊ satisfies H_D(P) ≤ E[L] < H_D(P) + 1 (Cover–Thomas).

Main definitions #

entropyD — D-ary Shannon entropy H_D(P) := −∑ a, P.real {a} · logb D P(a).
shannonLength — Shannon codeword length l(a) := ⌈−logb D P(a)⌉₊.
expectedLength — expected length E[L] := ∑ a, P.real {a} · l(a).
kraftSum — Kraft sum K_D(l) := ∑ a, D^{−l(a)}.

Main statements #

shannonLength_kraft_le_one — Shannon lengths satisfy Kraft: K_D(shannonLength) ≤ 1.
entropyD_le_expectedLength_of_kraft — Gibbs lower bound: Kraft-feasible l satisfies H_D(P) ≤ E[L].
expectedLength_shannon_lt_entropyD_add_one — Shannon upper bound (full support): E[L_Shannon] < H_D(P) + 1.
shannonCode_expected_length_bounds — sandwich: H_D(P) ≤ E[L_Shannon] < H_D(P) + 1.

Implementation notes #

The development works at the codeword-length level (α → ℕ) because Mathlib's kraft_mcmillan_inequality uses a Finset (List α) representation. The reverse direction (constructing a prefix code from a Kraft-feasible length function) is in ShannonCode/KraftReverse.lean. We use Real.logb D for the D-ary logarithm throughout, localizing the Real.log D factor. The upper bound (strict inequality) requires full support ∀ a, P.real {a} > 0; the lower bound does not.

Definitions #

noncomputable def

InformationTheory.Shannon.ShannonCode.entropyD

source

{α : Type u_1} [Fintype α] [MeasurableSpace α] (D : ℝ) (P : MeasureTheory.Measure α) :

ℝ

D-ary Shannon entropy (finite-alphabet, Real-valued): H_D(P) := -Σ a, P.real {a} · logb D P(a).

Equations

InformationTheory.Shannon.ShannonCode.entropyD D P = -∑ a : α, P.real {a} * Real.logb D (P.real {a})

Instances For

Used by

noncomputable def

InformationTheory.Shannon.ShannonCode.shannonLength

source

{α : Type u_1} [MeasurableSpace α] (D : ℝ) (P : MeasureTheory.Measure α) (a : α) :

ℕ

Shannon codeword length l(a) := ⌈−logb D P(a)⌉₊ : ℕ.

When P.real {a} = 0, Mathlib sets logb D 0 = 0 so l(a) = 0.

Equations

InformationTheory.Shannon.ShannonCode.shannonLength D P a = ⌈-Real.logb D (P.real {a})⌉₊

Instances For

Used by

noncomputable def

InformationTheory.Shannon.ShannonCode.expectedLength

source

{α : Type u_1} [Fintype α] [MeasurableSpace α] (P : MeasureTheory.Measure α) (l : α → ℕ) :

ℝ

Expected length E[L] := ∑ a, P.real {a} · l(a).

Equations

InformationTheory.Shannon.ShannonCode.expectedLength P l = ∑ a : α, P.real {a} * ↑(l a)

Instances For

Used by

noncomputable def

InformationTheory.Shannon.ShannonCode.kraftSum

source

{α : Type u_1} [Fintype α] (D : ℝ) (l : α → ℕ) :

ℝ

Kraft sum K_D(l) := ∑ a, D^{−l(a)} (Real-valued).

Equations

InformationTheory.Shannon.ShannonCode.kraftSum D l = ∑ a : α, D ^ (-↑(l a))

Instances For

Used by

Auxiliary lemmas #

theorem

InformationTheory.Shannon.ShannonCode.logb_le_div_log

source

{D x : ℝ} (hD : 1 < D) (hx : 0 < x) :

Real.logb D x ≤ (x - 1) / Real.log D

Gibbs log inequality in base D: logb D x ≤ (x − 1) / log D for D > 1, x > 0.

Used by

theorem

InformationTheory.Shannon.ShannonCode.rpow_neg_logb_eq

source

{D x : ℝ} (hD : 1 < D) (hx : 0 < x) :

D ^ (-Real.logb D x) = x⁻¹

D ^ (− logb D x) = x⁻¹ for D > 1, x > 0.

Used by

theorem

InformationTheory.Shannon.ShannonCode.rpow_natCast_shannonLength_ge_inv

source

{D : ℝ} (hD : 1 < D) {x : ℝ} (hx : 0 < x) :

x⁻¹ ≤ D ^ ↑⌈-Real.logb D x⌉₊

x⁻¹ ≤ D ^ ⌈−logb D x⌉₊ for D > 1, x > 0.

Used by

theorem

InformationTheory.Shannon.ShannonCode.zpow_neg_natCast_eq_rpow

source

{D : ℝ} :

0 < D → ∀ (l : ℕ), D ^ (-↑l) = D ^ (-↑l)

D ^ (−(l : ℤ)) = D ^ (−(l : ℝ)) for D > 0, l : ℕ.

Used by

Kraft feasibility of Shannon lengths #

theorem

InformationTheory.Shannon.ShannonCode.rpow_neg_shannonLength_le_real

source

{α : Type u_1} [MeasurableSpace α] (D : ℝ) (hD : 1 < D) (P : MeasureTheory.Measure α) {a : α} (ha : 0 < P.real {a}) :

D ^ (-↑(shannonLength D P a)) ≤ P.real {a}

D ^ (−shannonLength D P a) ≤ P.real {a} for P.real {a} > 0.

Used by

theorem

InformationTheory.Shannon.ShannonCode.shannonLength_kraft_le_one

source

{α : Type u_1} [Fintype α] [MeasurableSpace α] [MeasurableSingletonClass α] {D : ℝ} (hD : 1 < D) (P : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure P] (hP : ∀ (a : α), 0 < P.real {a}) :

kraftSum D (shannonLength D P) ≤ 1

Shannon code Kraft inequality: D > 1, P a probability measure with full support implies ∑ a, D ^ (−shannonLength D P a) ≤ 1.

Used by

Gibbs lower bound #

theorem

InformationTheory.Shannon.ShannonCode.entropyD_le_expectedLength_of_kraft

source

entropyD D P ≤ expectedLength P l

Gibbs lower bound: for D > 1, probability measure P with full support, and any Kraft-feasible lengths l, we have H_D(P) ≤ E[L].

Used by

Shannon upper bound #

theorem

InformationTheory.Shannon.ShannonCode.expectedLength_shannon_lt_entropyD_add_one

source

{α : Type u_1} [Fintype α] [Nonempty α] [MeasurableSpace α] [MeasurableSingletonClass α] {D : ℝ} (hD : 1 < D) (P : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure P] (hP : ∀ (a : α), 0 < P.real {a}) :

expectedLength P (shannonLength D P) < entropyD D P + 1

Shannon code upper bound: D > 1, probability measure P with full support ⟹ E[L_Shannon] < H_D(P) + 1.

Used by

Sandwich theorem #

theorem

InformationTheory.Shannon.ShannonCode.shannonCode_expected_length_bounds

source

entropyD D P ≤ expectedLength P (shannonLength D P) ∧ expectedLength P (shannonLength D P) < entropyD D P + 1

Shannon code sandwich (Cover–Thomas): for a probability measure P with full support on a finite alphabet, the Shannon codeword lengths satisfy H_D(P) ≤ E[L_Shannon] < H_D(P) + 1.

Used by