Shannon's source coding theorem

AbbreviationPrefix-free code (Shannon source coding)#✓fully proved

A code \(c\) assigning to each element of \(\alpha\) a finite word over \(\beta\) is prefix-free when, for all distinct \(a_1, a_2 \in \alpha\), the word \(c(a_1)\) is not a prefix of the word \(c(a_2)\). This is the general notion of a prefix-free code.

abbrev IsPrefixFree {α β : Type*} (code : α → List β) : Prop :=
  MathlibExt.InformationTheory.IsPrefixFree code

Uses 1 · Used by 1

Statement usesPrefix-free code

Used byShannon source coding upper bound

TheoremShannon source coding lower bound#✓fully proved

Let \(\alpha\) and \(\beta\) be finite types with \(q = |\beta| \ge 2\), and let \(p : \alpha \to \mathbb{R}\) satisfy \(p(a) > 0\) for every \(a \in \alpha\) and \(\sum_{a \in \alpha} p(a) = 1\). Let \(c\) assign to each \(a \in \alpha\) a finite word \(c(a)\) over \(\beta\), of length \(|c(a)|\), such that \(c\) is injective and its set of codewords is uniquely decodable: any two finite lists of codewords with the same concatenation are equal. Then the expected length \(\sum_{a \in \alpha} p(a)\,|c(a)|\) is at least the base-\(q\) entropy \(-\left(\sum_{a \in \alpha} p(a) \log p(a)\right) / \log q\), where \(\log\) is the natural logarithm.

theorem shannon_source_coding_lower_bound
    {α β : Type*} [Fintype α] [Fintype β]
    (p : α → ℝ)
    (hp_pos : ∀ a, 0 < p a)
    (hp_sum : ∑ a : α, p a = 1)
    (hq : 2 ≤ Fintype.card β)
    (code : α → List β)
    (h_inj : Function.Injective code)
    (h_ud : InformationTheory.IsUniquelyDecodable (Set.range code)) :
    -(∑ a : α, p a * Real.log (p a)) / Real.log (Fintype.card β : ℝ)
      ≤ ∑ a : α, p a * ((code a).length : ℝ)

Sources

C. E. Shannon, Bell Syst. Tech. J. 27 (1948), 379-423 and 623-656, DOI 10.1002/j.1538-7305.1948.tb01338.x.

TheoremShannon source coding upper bound#✓fully proved

Let \(\alpha\) and \(\beta\) be finite types with \(q = |\beta| \ge 2\), and let \(p : \alpha \to \mathbb{R}\) satisfy \(p(a) > 0\) for every \(a \in \alpha\) and \(\sum_{a \in \alpha} p(a) = 1\). Then there is a prefix-free code \(c\) assigning to each \(a \in \alpha\) a finite word \(c(a)\) over \(\beta\), of length \(|c(a)|\), whose expected length \(\sum_{a \in \alpha} p(a)\,|c(a)|\) is strictly less than \(-\left(\sum_{a \in \alpha} p(a) \log p(a)\right) / \log q + 1\), where \(\log\) is the natural logarithm.

theorem shannon_source_coding_upper_bound
    {α β : Type*} [Fintype α] [Fintype β]
    (p : α → ℝ)
    (hp_pos : ∀ a, 0 < p a)
    (hp_sum : ∑ a : α, p a = 1)
    (hq : 2 ≤ Fintype.card β) :
    ∃ (code : α → List β),
      IsPrefixFree code ∧
        (∑ a : α, p a * ((code a).length : ℝ)) <
          -(∑ a : α, p a * Real.log (p a)) / Real.log (Fintype.card β : ℝ) + 1

Sources

C. E. Shannon, Bell Syst. Tech. J. 27 (1948), 379-423 and 623-656, DOI 10.1002/j.1538-7305.1948.tb01338.x.

Uses 3

Statement usesPrefix-free code (Shannon source coding)

Proof usesPrefix-free code · Kraft's inequality for prefix codes

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.