Kraft's Inequality

This file proves Kraft's inequality for prefix-free codes over finite alphabets. The finite result is an immediate consequence of the Kraft–McMillan inequality; the result for arbitrary sets of codewords follows by bounding every finite partial sum.

Main results

• IsPrefixFree.finsetSum_one_div_card_pow_length_le_one: the Kraft sum of a finite prefix-free code is at most one.
• IsPrefixFree.summable_one_div_card_pow_length: the Kraft sum of an arbitrary prefix-free code is summable.
• IsPrefixFree.tsum_one_div_card_pow_length_le_one: the Kraft sum of an arbitrary prefix-free code is at most one.

References

• Cover and Thomas, Elements of Information Theory, Chapter 5.

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

Kraft's inequality. The Kraft sum of a finite prefix-free code is at most one.

theorem InformationTheory.IsPrefixFree.summable_one_div_card_pow_length {α : Type u_1} [Fintype α] [Nonempty α] {S : Set (List α)} (hS : IsPrefixFree S) : Summable fun (w : ↑S) => (1 / ↑(Fintype.card α)) ^ (↑w).length

The Kraft sum of an arbitrary prefix-free code is summable.

theorem InformationTheory.IsPrefixFree.tsum_one_div_card_pow_length_le_one {α : Type u_1} [Fintype α] [Nonempty α] {S : Set (List α)} (hS : IsPrefixFree S) : ∑' (w : ↑S), (1 / ↑(Fintype.card α)) ^ (↑w).length ≤ 1

Kraft's inequality for arbitrary codes. The Kraft sum of an arbitrary prefix-free code is at most one.