Uniquely Decodable Codes

This file defines uniquely decodable codes and proves basic properties.

Main definitions

• UniquelyDecodable: A set of codewords is uniquely decodable if distinct concatenations of codewords yield distinct strings.

Main results

• UniquelyDecodable.epsilon_not_mem: Uniquely decodable codes cannot contain the empty string.
• UniquelyDecodable.flatten_injective: The flatten function is injective on lists of codewords from a uniquely decodable code.

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

A set of lists is uniquely decodable if distinct concatenations yield distinct strings.

Equations

• InformationTheory.UniquelyDecodable S = ∀ (L₁ L₂ : List (List α)), (∀ (w : List α), w ∈ L₁ → w ∈ S) → (∀ (w : List α), w ∈ L₂ → w ∈ S) → L₁.flatten = L₂.flatten → L₁ = L₂

theorem InformationTheory.UniquelyDecodable.epsilon_not_mem {α : Type u_1} {S : Set (List α)} (h : UniquelyDecodable S) : ¬[] ∈ S

If a code is uniquely decodable, it does not contain the empty string.

The empty string can be "decoded" as either zero or two copies of itself, violating unique decodability.

theorem InformationTheory.UniquelyDecodable.flatten_injective {α : Type u_1} {S : Set (List α)} (h : UniquelyDecodable S) : Function.Injective fun (L : { L : List (List α) // ∀ (x : List α), x ∈ L → x ∈ S }) => (↑L).flatten