Source coding

Lossless compression of information sources by variable-length codes, including prefix codes, the Kraft–McMillan inequality and Shannon's source coding bounds.

• Prefix codes
• Huffman coding
• Run-length encoding
• Shannon's source coding theorem

TheoremKraft's inequality for prefix codes#✓fully proved

Let \(\alpha\) be a finite set of source symbols, let \(\beta\) be a finite alphabet with \(D \ge 2\) letters, and let \(l : \alpha \to \mathbb{N}\). There is a prefix-free code assigning to each \(a \in \alpha\) a word over \(\beta\) of length \(l(a)\) if and only if \(\sum_{a \in \alpha} D^{-l(a)} \le 1\).

public theorem kraft_mcmillan_lengths {α β : Type*} [Fintype α] [Fintype β]
    (l : α → ℕ) (hq : 2 ≤ Fintype.card β) :
    (∃ code : α → List β, IsPrefixFree code ∧ ∀ a, (code a).length = l a)
      ↔ ∑ a : α, (1 : ℝ) / (Fintype.card β : ℝ) ^ (l a) ≤ 1

Uses 3 · Used by 1

Statement usesPrefix-free code

Proof usesA prefix-free code with an empty codeword has one symbol · Prefix-free codes are injective

Used byShannon source coding upper bound

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.