Kraft–McMillan inequality

The definition InformationTheory.UniquelyDecodable applied to a set S of lists over a type α asserts the following universally quantified statement: for all pairs of finite lists of lists L₁ and L₂ (i.e., L₁ and L₂ are each finite sequences whose entries are themselves lists over α — "codewords"), if every entry w of L₁ belongs to S and every entry w of L₂ belongs to S, and if concatenating (flattening) all the lists in L₁ in order yields the same single list as concatenating (flattening) all the lists in L₂ in order, then L₁ and L₂ are equal as lists (same length, same entries in the same order). Note L₁ and L₂ range over arbitrary finite sequences of codewords drawn from S — including the empty sequence, and allowing repeated codewords and any ordering — with no bound on their length; equality of L₁ and L₂ is equality of sequences of codewords, which is strictly stronger than merely producing the same flattened list.

The theorem kraft_mcmillan_inequality fixes a type α (with a Fintype α instance, hence finite, and a Nonempty α instance, hence Fintype.card α ≥ 1) and a finite set S : Finset (List α), i.e., a finite collection of finite lists ("codewords") over the alphabet α. Its hypothesis h is exactly the statement InformationTheory.UniquelyDecodable (S : Set (List α)) as unfolded above, applied to S coerced to a Set (List α). Its conclusion is that the sum, taken over all codewords w in the finite set S, of $\left(\dfrac{1}{|\alpha|}\right)^{\operatorname{length}(w)}$ — where $|\alpha|$ denotes Fintype.card α, the number of elements of α, and $\operatorname{length}(w)$ is the length of the list w — is at most $1$; formally, $\sum_{w \in S} \left(\dfrac{1}{|\alpha|}\right)^{|w|} \le 1$, where the sum, base, and exponent are all real numbers (the exponentiation is real-number exponentiation of a real base by a natural-number exponent, w.length : ℕ). Note that since α is nonempty, Fintype.card α ≥ 1, so 1 / (Fintype.card α : ℝ) is well-defined and lies in (0, 1] (no division-by-zero degeneracy); if S is empty the sum is the empty sum 0 ≤ 1, and if S contains the empty list [] (length 0), that term contributes (1/|α|)^0 = 1 to the sum.