Prefix codes

DefinitionPrefix-free code#✓fully proved

A code \(c\) assigning to each source symbol a finite word over an alphabet is prefix-free if for all distinct symbols \(a_1 \ne a_2\) the word \(c(a_1)\) is not a prefix of \(c(a_2)\). Since the condition covers all ordered pairs of distinct symbols, both prefix directions are forbidden.

def IsPrefixFree {α β : Type*} (code : α → List β) : Prop :=
  ∀ ⦃a₁ a₂ : α⦄, a₁ ≠ a₂ → ¬ code a₁ <+: code a₂

Used by 8

Used byHuffman codes are prefix-free · Huffman tree codes are prefix-free · Kraft's inequality for prefix codes · Prefix-related codewords come from the same symbol · A prefix-free code with an empty codeword has one symbol · Prefix-free codes are injective · Prefix-free code (Shannon source coding) · Shannon source coding upper bound

TheoremPrefix-related codewords come from the same symbol#✓fully proved

If \(c\) is a prefix-free code and the codeword \(c(a_1)\) is a prefix of \(c(a_2)\), then \(a_1 = a_2\).

theorem IsPrefixFree.eq_of_isPrefix {α β : Type*} {code : α → List β}
    (h : IsPrefixFree code) {a₁ a₂ : α} (hpre : code a₁ <+: code a₂) :
    a₁ = a₂

Uses 1

Statement usesPrefix-free code

TheoremPrefix-free codes are injective#✓fully proved

If \(c\) is a prefix-free code and \(c(a_1) = c(a_2)\), then \(a_1 = a_2\).

Equal codewords are mutually prefix, hence come from equal symbols.

theorem IsPrefixFree.injective {α β : Type*} {code : α → List β}
    (h : IsPrefixFree code) : Function.Injective code

Uses 1 · Used by 1

Statement usesPrefix-free code

Used byKraft's inequality for prefix codes

TheoremA prefix-free code with an empty codeword has one symbol#✓fully proved

If a prefix-free code \(c\) assigns the empty word to a symbol \(a_0\), then every symbol \(a\) equals \(a_0\).

This holds because the empty word is a prefix of every word.

theorem IsPrefixFree.eq_of_mem_nil {α β : Type*} {code : α → List β}
    (h : IsPrefixFree code) {a₀ : α} (ha₀ : code a₀ = []) (a : α) :
    a = a₀

Uses 1 · Used by 1

Statement usesPrefix-free code

Used byKraft's inequality for prefix codes

4 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.