Shannon's source coding theorem for a source with at least two symbols
ProvedSourceCoding.shannon_source_coding_theorem_of_two_le_cardLet be a probability distribution on a finite set of source symbols with at least two symbols, and , and let be a code alphabet with letters. Write for the base- entropy (the platform definition SourceCoding.entropy). Then:
- every injective assignment of codewords whose codeword set is uniquely decodable has expected length at least the entropy,
- there is an injective assignment of codewords with uniquely decodable codeword set whose expected length is strictly less than the entropy plus one,
This is Shannon's source coding theorem in the form (Cover and Thomas, Elements of Information Theory, Theorem 5.4.1). The lower bound follows from the Kraft–McMillan inequality and Gibbs' inequality; the upper bound is attained by the Shannon–Fano lengths , which satisfy Kraft's inequality and are positive precisely because every , which is where the hypothesis is used. Without that hypothesis the second part fails for the one-symbol source (entropy , but no uniquely decodable code has a codeword of length ), which is why the earlier platform statement SourceCoding.shannon_source_coding_theorem was disproved.
import Mathlib import Definitions.Def_SourceCoding_entropy
namespace SourceCoding
/-- **Shannon's source coding theorem** (Shannon 1948; Cover--Thomas, Theorem 5.4.1), for a
source with at least two symbols. Every uniquely decodable injective code has expected length at
least the base-`D` entropy, and some uniquely decodable injective code has expected length
strictly less than the entropy plus one. -/
theorem shannon_source_coding_theorem_of_two_le_card
{ι : Type} [Fintype ι] (hι : 2 ≤ Fintype.card ι) (p : ι → ℝ) (hp_pos : ∀ i, 0 < p i)
(hp_sum : ∑ i, p i = 1)
{α : Type} [Fintype α] [Nonempty α] (hD : 2 ≤ Fintype.card α) :
(∀ c : ι → List α, Function.Injective c →
InformationTheory.UniquelyDecodable (Set.range c) →
entropy p (Fintype.card α) ≤ ∑ i, p i * (c i).length) ∧
(∃ c : ι → List α, Function.Injective c ∧
InformationTheory.UniquelyDecodable (Set.range c) ∧
∑ i, p i * (c i).length < entropy p (Fintype.card α) + 1) := by sorry
end SourceCoding