Uniquely Decodable Codes

This file defines uniquely decodable codes and proves basic properties.

Main definitions

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

Main results

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

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

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

Equations

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

@[deprecated InformationTheory.IsUniquelyDecodable (since := "2026-08-16")]

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

Alias of InformationTheory.IsUniquelyDecodable.

---

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

Equations

• @InformationTheory.UniquelyDecodable = @InformationTheory.IsUniquelyDecodable

theorem InformationTheory.IsUniquelyDecodable.epsilon_not_mem {α : Type u_1} {S : Set (List α)} (h : IsUniquelyDecodable 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.

@[deprecated InformationTheory.IsUniquelyDecodable.epsilon_not_mem (since := "2026-08-16")]

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

Alias of InformationTheory.IsUniquelyDecodable.epsilon_not_mem.

---

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.IsUniquelyDecodable.flatten_injective {α : Type u_1} {S : Set (List α)} (h : IsUniquelyDecodable S) : Function.Injective fun (L : { L : List (List α) // ∀ (x : List α), x ∈ L → x ∈ S }) => (↑L).flatten

@[deprecated InformationTheory.IsUniquelyDecodable.flatten_injective (since := "2026-08-16")]

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

Alias of InformationTheory.IsUniquelyDecodable.flatten_injective.