Skip to content

InformationTheory.Shannon.ShannonCode.KraftReverse

Imports 8

Kraft inequality converse: existence of prefix codes #

Converse direction of Cover–Thomas (McMillan converse): if a length function l : α → ℕ satisfies the Kraft inequality ∑_a D^{−l(a)} ≤ 1, then there exists a prefix-free code c : α → List (Fin D) with (c a).length = l a for all a.

Main statements #

exists_prefix_code_of_kraft — Kraft-feasible lengths (D ≥ 2, 0 < l a) yield an injective prefix-free code with the prescribed lengths.

Implementation notes #

The proof uses a greedy (Shannon–Fano) construction: sort α by l in ascending order (sortedByLen), compute a cumulative slot offset slotStart k := ∑_{j < k} D^(L − l (as[j])) at a common depth L = sup l, and define c(a) := toBaseDLen D (l a) (slotStart (idx a) / D^(L − l a)). Here toBaseDLen D L n is the MSB-first length-L base-D digit expansion of n. Prefix-freeness follows from a gap argument on slotStart.

Definitions #

def

InformationTheory.Shannon.ShannonCodeKraftReverse.toBaseDLen

(D : ℕ) [NeZero D] (L n : ℕ) :

MSB-first base-D digit expansion of length L of n.

For n < D^L, this is the canonical length-L digit list (most-significant first).

Equations

InformationTheory.Shannon.ShannonCodeKraftReverse.toBaseDLen D L n = List.ofFn fun (i : Fin L) => ⟨n / D ^ (L - 1 - ↑i) % D, ⋯⟩

Instances For

Used by

def

InformationTheory.Shannon.ShannonCodeKraftReverse.IsPrefixFree

{α : Type u_1} {D : ℕ} (c : α → List (Fin D)) :

Predicate asserting that c is prefix-free: no codeword is a proper prefix of another.

Equations

InformationTheory.Shannon.ShannonCodeKraftReverse.IsPrefixFree c = ∀ (a b : α), a ≠ b → ¬c a <+: c b

Instances For

Used by

Properties of `toBaseDLen` #

theorem

InformationTheory.Shannon.ShannonCodeKraftReverse.toBaseDLen_length

@[simp]

(D : ℕ) [NeZero D] (L n : ℕ) :

(toBaseDLen D L n).length = L

Length of toBaseDLen D L n is L.

Used by

theorem

InformationTheory.Shannon.ShannonCodeKraftReverse.toBaseDLen_take

(D : ℕ) [NeZero D] {L₁ L₂ : ℕ} (h : L₁ ≤ L₂) (n : ℕ) :

List.take L₁ (toBaseDLen D L₂ n) = toBaseDLen D L₁ (n / D ^ (L₂ - L₁))

The top-L₁ digits of toBaseDLen D L₂ n equal toBaseDLen D L₁ (n / D^(L₂ − L₁)) when L₁ ≤ L₂ (MSB-first prefix property).

Used by

theorem

InformationTheory.Shannon.ShannonCodeKraftReverse.toBaseDLen_eq_of_isPrefix

(D : ℕ) [NeZero D] {L₁ L₂ : ℕ} (h : L₁ ≤ L₂) {n₁ n₂ : ℕ} (hpref : toBaseDLen D L₁ n₁ <+: toBaseDLen D L₂ n₂) :

toBaseDLen D L₁ n₁ = toBaseDLen D L₁ (n₂ / D ^ (L₂ - L₁))

If toBaseDLen D L₁ n₁ is a prefix of toBaseDLen D L₂ n₂ and L₁ ≤ L₂, then toBaseDLen D L₁ n₁ = toBaseDLen D L₁ (n₂ / D ^ (L₂ − L₁)).

Used by

theorem

InformationTheory.Shannon.ShannonCodeKraftReverse.toBaseDLen_injOn_lt

(D : ℕ) [NeZero D] (L : ℕ) {n₁ n₂ : ℕ} (h₁ : n₁ < D ^ L) (h₂ : n₂ < D ^ L) (heq : toBaseDLen D L n₁ = toBaseDLen D L n₂) :

n₁ = n₂

Strict variant: if n₁, n₂ < D^L, toBaseDLen D L n₁ = toBaseDLen D L n₂ ⟹ n₁ = n₂.

Used by

Greedy construction #

noncomputable def

InformationTheory.Shannon.ShannonCodeKraftReverse.sortedByLen

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

Elements of α sorted by l in ascending order.

Equations

InformationTheory.Shannon.ShannonCodeKraftReverse.sortedByLen l = Finset.univ.toList.mergeSort fun (a b : α) => decide (l a ≤ l b)

Instances For

Used by

theorem

InformationTheory.Shannon.ShannonCodeKraftReverse.sortedByLen_length

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

(sortedByLen l).length = Fintype.card α

Used by

theorem

InformationTheory.Shannon.ShannonCodeKraftReverse.mem_sortedByLen

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

a ∈ sortedByLen l

Used by

theorem

InformationTheory.Shannon.ShannonCodeKraftReverse.sortedByLen_pairwise_le

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

List.Pairwise (fun (a b : α) => l a ≤ l b) (sortedByLen l)

Used by

noncomputable def

InformationTheory.Shannon.ShannonCodeKraftReverse.slotStart

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

Cumulative slot offset: slotStart D l L k = ∑_{j < k} D^(L − l (sortedByLen l)[j]). Saturates to the full sum for k ≥ |α|.

Equations

One or more equations did not get rendered due to their size.

Instances For

Used by

theorem

InformationTheory.Shannon.ShannonCodeKraftReverse.slotStart_mono

{α : Type u_1} [Fintype α] (D : ℕ) (l : α → ℕ) (L : ℕ) {k₁ k₂ : ℕ} (h : k₁ ≤ k₂) :

slotStart D l L k₁ ≤ slotStart D l L k₂

slotStart is monotone in k.

Used by

theorem

InformationTheory.Shannon.ShannonCodeKraftReverse.slotStart_succ

{α : Type u_1} [Fintype α] (D : ℕ) (l : α → ℕ) (L : ℕ) {k : ℕ} (hk : k < (sortedByLen l).length) :

slotStart D l L (k + 1) = slotStart D l L k + D ^ (L - l (sortedByLen l)[k])

slotStart (k+1) = slotStart k + D^(L - l (as[k])).

Used by

theorem

InformationTheory.Shannon.ShannonCodeKraftReverse.slotStart_of_ge

{α : Type u_1} [Fintype α] (D : ℕ) (l : α → ℕ) (L : ℕ) {k : ℕ} (hk : (sortedByLen l).length ≤ k) :

slotStart D l L k = slotStart D l L (sortedByLen l).length

slotStart stabilizes when k ≥ (sortedByLen l).length.

Used by

theorem

InformationTheory.Shannon.ShannonCodeKraftReverse.slotStart_card_eq_sum

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

slotStart D l L (Fintype.card α) = ∑ a : α, D ^ (L - l a)

slotStart at Fintype.card α equals the full sum ∑ a : α, D ^ (L − l a).

Used by

Slot upper bound from the Kraft condition #

theorem

InformationTheory.Shannon.ShannonCodeKraftReverse.kraft_sum_nat_le_of_real

{α : Type u_1} [Fintype α] {D : ℕ} (hD : 2 ≤ D) (l : α → ℕ) (L : ℕ) (hL : ∀ (a : α), l a ≤ L) (hk : ∑ a : α, ↑D ^ (-↑(l a)) ≤ 1) :

∑ a : α, D ^ (L - l a) ≤ D ^ L

The Kraft condition implies ∑_a D^(L − l(a)) ≤ D^L as a natural number inequality.

Used by

theorem

InformationTheory.Shannon.ShannonCodeKraftReverse.slotStart_le_pow

{α : Type u_1} [Fintype α] {D : ℕ} (hD : 2 ≤ D) (l : α → ℕ) (L : ℕ) (hL : ∀ (a : α), l a ≤ L) (hk : ∑ a : α, ↑D ^ (-↑(l a)) ≤ 1) (k : ℕ) :

slotStart D l L k ≤ D ^ L

slotStart D l L k ≤ D ^ L for all k.

Used by

Code construction and main theorem #

noncomputable def

InformationTheory.Shannon.ShannonCodeKraftReverse.sortedIndex

{α : Type u_1} [Fintype α] [DecidableEq α] (l : α → ℕ) (a : α) :

Position of a in sortedByLen l.

Equations

InformationTheory.Shannon.ShannonCodeKraftReverse.sortedIndex l a = List.idxOf a (InformationTheory.Shannon.ShannonCodeKraftReverse.sortedByLen l)

Instances For

Used by

theorem

InformationTheory.Shannon.ShannonCodeKraftReverse.sortedIndex_lt

{α : Type u_1} [Fintype α] [DecidableEq α] (l : α → ℕ) (a : α) :

sortedIndex l a < (sortedByLen l).length

Used by

theorem

InformationTheory.Shannon.ShannonCodeKraftReverse.getElem_sortedByLen_sortedIndex

{α : Type u_1} [Fintype α] [DecidableEq α] (l : α → ℕ) (a : α) :

(sortedByLen l)[sortedIndex l a] = a

Used by

theorem

InformationTheory.Shannon.ShannonCodeKraftReverse.sortedIndex_injective

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

Function.Injective (sortedIndex l)

Used by

noncomputable def

InformationTheory.Shannon.ShannonCodeKraftReverse.shannonFanoCode

{α : Type u_1} [Fintype α] [DecidableEq α] {D : ℕ} [NeZero D] (l : α → ℕ) (L : ℕ) (a : α) :

Main code construction: the Shannon–Fano codeword for a.

Equations

One or more equations did not get rendered due to their size.

Instances For

Used by

theorem

InformationTheory.Shannon.ShannonCodeKraftReverse.shannonFanoCode_length

@[simp]

{α : Type u_1} [Fintype α] [DecidableEq α] {D : ℕ} [NeZero D] (l : α → ℕ) (L : ℕ) (a : α) :

(shannonFanoCode l L a).length = l a

Used by

theorem

InformationTheory.Shannon.ShannonCodeKraftReverse.slotStart_gap

{α : Type u_1} [Fintype α] (D : ℕ) (l : α → ℕ) (L : ℕ) {j k : ℕ} (hjk : j < k) (hk : k ≤ (sortedByLen l).length) :

slotStart D l L j + D ^ (L - l (sortedByLen l)[j]) ≤ slotStart D l L k

For j < k ≤ |sortedByLen l|, slotStart j + D^(L − l (as[j])) ≤ slotStart k.

Used by

theorem

InformationTheory.Shannon.ShannonCodeKraftReverse.slotStart_lt_pow_of_lt

{α : Type u_1} [Fintype α] {D : ℕ} (hD : 2 ≤ D) (l : α → ℕ) (L : ℕ) (hL : ∀ (a : α), l a ≤ L) (hk_real : ∑ a : α, ↑D ^ (-↑(l a)) ≤ 1) {j : ℕ} (hj : j < (sortedByLen l).length) :

slotStart D l L j < D ^ L

slotStart D l L j < D ^ L for j < (sortedByLen l).length.

Used by

theorem

InformationTheory.Shannon.ShannonCodeKraftReverse.not_isPrefix_of_sortedIndex_lt

{α : Type u_1} [Fintype α] [DecidableEq α] {D : ℕ} [NeZero D] (hD : 2 ≤ D) (l : α → ℕ) (L : ℕ) (hL : ∀ (a : α), l a ≤ L) (hk_real : ∑ a : α, ↑D ^ (-↑(l a)) ≤ 1) {x y : α} (h_idx_lt : sortedIndex l x < sortedIndex l y) (h_len_le : l x ≤ l y) :

¬shannonFanoCode l L x <+: shannonFanoCode l L y

When sortedIndex l x < sortedIndex l y and l x ≤ l y, the code of x is not a prefix of the code of y.

Used by

theorem

InformationTheory.Shannon.ShannonCodeKraftReverse.shannonFanoCode_prefixFree

{α : Type u_1} [Fintype α] [DecidableEq α] {D : ℕ} [NeZero D] (hD : 2 ≤ D) (l : α → ℕ) (_hl : ∀ (a : α), 0 < l a) (L : ℕ) (hL : ∀ (a : α), l a ≤ L) (hk : ∑ a : α, ↑D ^ (-↑(l a)) ≤ 1) :

IsPrefixFree (shannonFanoCode l L)

shannonFanoCode is prefix-free. (The hypothesis hl : 0 < l a is redundant given hk but is kept for API uniformity.)

Used by

theorem

InformationTheory.Shannon.ShannonCodeKraftReverse.shannonFanoCode_injective

{α : Type u_1} [Fintype α] [DecidableEq α] {D : ℕ} [NeZero D] (hD : 2 ≤ D) (l : α → ℕ) (hl : ∀ (a : α), 0 < l a) (L : ℕ) (hL : ∀ (a : α), l a ≤ L) (hk : ∑ a : α, ↑D ^ (-↑(l a)) ≤ 1) :

Function.Injective (shannonFanoCode l L)

shannonFanoCode is injective.

Used by

noncomputable def

InformationTheory.Shannon.ShannonCodeKraftReverse.commonDepth

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

Common depth: sup_{a} l a, the maximum codeword length.

Equations

InformationTheory.Shannon.ShannonCodeKraftReverse.commonDepth l = Finset.univ.sup l

Instances For

Used by

theorem

InformationTheory.Shannon.ShannonCodeKraftReverse.le_commonDepth

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

l a ≤ commonDepth l

Used by

theorem

InformationTheory.Shannon.ShannonCodeKraftReverse.exists_prefix_code_of_kraft

{α : Type u_1} [Fintype α] {D : ℕ} (hD : 2 ≤ D) (l : α → ℕ) (hl : ∀ (a : α), 0 < l a) (hk : ∑ a : α, ↑D ^ (-↑(l a)) ≤ 1) :

∃ (c : α → List (Fin D)), Function.Injective c ∧ (∀ (a : α), (c a).length = l a) ∧ IsPrefixFree c

Kraft converse: Kraft-feasible positive lengths yield a prefix-free code.

Used by