Commit 2026-08-24 11:13 8aca7eba

feat(InformationTheory/Coding): add Kraft inequality for prefix-free codes (#42584) This PR defines prefix-free codes as arbitrary sets of words and proves that a prefix-free code not containing the empty word is uniquely decodable. In particular, every nontrivial prefix-free code is uniquely decodable. It is a direct continuation of #34108, which introduced uniquely decodable codes and the Kraft–McMillan inequality. For a finite nonempty alphabet, it derives Kraft's inequality for finite prefix-free codes from the Kraft–McMillan inequality. It then extends the result to arbitrary sets of codewords by bounding every finite partial sum, proving summability and the corresponding bound on the infinite Kraft sum. The existing uniquely decodable code API is also renamed to follow the Is... naming convention, and the Kraft–McMillan theorem is renamed to describe its statement. Moves:

• InformationTheory.UniquelyDecodable -> InformationTheory.IsUniquelyDecodable
• InformationTheory.UniquelyDecodable.epsilon_not_mem -> InformationTheory.IsUniquelyDecodable.epsilon_not_mem
• InformationTheory.UniquelyDecodable.flatten_injective -> InformationTheory.IsUniquelyDecodable.flatten_injective
• InformationTheory.kraft_mcmillan_inequality -> InformationTheory.IsUniquelyDecodable.finsetSum_one_div_card_pow_length_le_one