Commit 2026-02-17 15:39 1829e3ff

feat(InformationTheory/Coding): Kraft-McMillan inequality for uniquely decodable codes (#34108) This PR introduces the basic definition of uniquely decodable codes and proves the Kraft-McMillan inequality, a fundamental result in noiseless coding theory. The results live in the InformationTheory namespace, in the directory InformationTheory/Coding.

Main definitions

• InformationTheory.UniquelyDecodable: a set of codewords is uniquely decodable if concatenation is injective on finite lists of codewords.

Main results

• InformationTheory.kraft_mcmillan_inequality: for any finite uniquely decodable code S over an alphabet of size D, $\sum_{w \in S} D^{-|w|} \le 1.$
• InformationTheory.UniquelyDecodable.epsilon_not_mem: uniquely decodable codes cannot contain the empty string.