Kraft-McMillan Inequality

This file proves the Kraft-McMillan inequality for uniquely decodable codes.

Main definitions

• concatFn: Concatenation of r codewords into a single string.

Main results

• IsUniquelyDecodable.finsetSum_one_div_card_pow_length_le_one: For a uniquely decodable code S over an alphabet of size D, ∑_{w ∈ S} D^{-|w|} ≤ 1.

The proof uses a counting argument: the r-th power of the Kraft sum counts concatenations of r codewords, weighted by length. Since the code is uniquely decodable, these concatenations are distinct, and the count is bounded by the number of strings of each length.

References

• McMillan, B. (1956), "Two inequalities implied by unique decipherability"

theorem InformationTheory.IsUniquelyDecodable.finsetSum_one_div_card_pow_length_le_one {α : Type u_1} {S : Finset (List α)} [Fintype α] [Nonempty α] (h : IsUniquelyDecodable ↑S) : ∑ w ∈ S, (1 / ↑(Fintype.card α)) ^ w.length ≤ 1

Kraft-McMillan Inequality: If S is a finite uniquely decodable code, then Σ D^{-|w|} ≤ 1.

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

theorem InformationTheory.kraft_mcmillan_inequality {α : Type u_1} {S : Finset (List α)} [Fintype α] [Nonempty α] (h : IsUniquelyDecodable ↑S) : ∑ w ∈ S, (1 / ↑(Fintype.card α)) ^ w.length ≤ 1

Alias of InformationTheory.IsUniquelyDecodable.finsetSum_one_div_card_pow_length_le_one.

---

Kraft-McMillan Inequality: If S is a finite uniquely decodable code, then Σ D^{-|w|} ≤ 1.