Prefix-Free Codes

This file defines prefix-free codes and proves that every prefix-free code not containing the empty word is uniquely decodable.

Main definitions

• IsPrefixFree: a set of words is prefix-free if two words in the set cannot be distinct when one is a prefix of the other.

Main results

• IsPrefixFree.isUniquelyDecodable: a prefix-free code not containing the empty word is uniquely decodable.

def InformationTheory.IsPrefixFree {α : Type u_1} (S : Set (List α)) : Prop

A set of words is prefix-free if two words in the set cannot be distinct when one is a prefix of the other.

Equations

• InformationTheory.IsPrefixFree S = ∀ (x : List α), x ∈ S → ∀ (y : List α), y ∈ S → x <+: y → x = y

theorem InformationTheory.IsPrefixFree.eq_singleton_empty_of_empty_mem {α : Type u_1} {S : Set (List α)} (hS : IsPrefixFree S) (hε : [] ∈ S) : S = {[]}

A prefix-free set containing the empty word is the singleton containing the empty word.

theorem InformationTheory.IsPrefixFree.anti {α : Type u_1} {S T : Set (List α)} (hS : IsPrefixFree S) (hTS : T ⊆ S) : IsPrefixFree T

Any subset of a prefix-free set is prefix-free.

theorem InformationTheory.IsPrefixFree.isUniquelyDecodable {α : Type u_1} {S : Set (List α)} (hS : IsPrefixFree S) (hε : ¬[] ∈ S) : IsUniquelyDecodable S

A prefix-free code not containing the empty word is uniquely decodable.

theorem InformationTheory.IsPrefixFree.isUniquelyDecodable_of_nontrivial {α : Type u_1} {S : Set (List α)} (hS : IsPrefixFree S) (hS' : S.Nontrivial) : IsUniquelyDecodable S

A nontrivial prefix-free code is uniquely decodable.