TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck pass

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Shannon bounds for finite binary codes

Statement

Let $p$ be a finite full-support source and let $H_{2} (p)$ be its entropy in bits. Every finite binary uniquely decodable code $C$ satisfies $L_{p} (C) \geq H_{2} (p)$ . If $m \geq 2$ , the binary prefix code with lengths $ℓ_{i} = ⌈ - \log_{2} p_{i} ⌉$ (called a Shannon code) has expected length strictly less than $H_{2} (p) + 1$ . If $m = 1$ , the one-bit codeword $0$ has length $1 = H_{2} (p) + 1$ .

Facts & Assumptions

Given: A finite full-support source $p = (p_{i})_{i = 1}^{m}$ and a finite binary code $C$ .

[F1]

Finite discrete sources and product blocks: $m \geq 1$ , $p_{i} > 0$ , and $\sum_{i} p_{i} = 1$ .

[F2]

Base-two entropy of a finite source: $H_{2} (p) = H (p) / \ln 2 = - \sum_{i} p_{i} \log_{2} p_{i}$ .

[F3]

Finite binary source codes, extension, and expected length: $L_{p} (C) = \sum_{i} p_{i} ℓ_{i}$ , and $C$ is uniquely decodable exactly when its finite-word concatenation extension is injective.

[F4]

McMillan inequality for finite binary uniquely decodable codes: Every finite binary uniquely decodable code has $\sum_{i} 2^{- ℓ_{i}} \leq 1$ .

[F5]

Nonnegativity of finite relative entropy with a positive reference: For finite probability vectors $p, q$ with $q_{i} > 0$ , $D (p ∥ q) \geq 0$ .

[F6]

Binary Kraft criterion for finite positive codeword lengths: Positive integer lengths are realized by a binary prefix code whenever their Kraft sum is at most one.

[F7]

Finite distributions, entropy, divergence, and stochastic matrices: $H (p) : = - \sum_{i} p_{i} \ln p_{i}$ and $D (p ∥ q) : = \sum_{i : p_{i} > 0} p_{i} \ln (p_{i} / q_{i})$ when $q_{i} > 0$ .

[F8]

Information units and logarithm-base convention: $\log_{2} x = \ln x / \ln 2$ , and $\ln 2 > 0$ .

[F9]

Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm: $\ln$ is strictly increasing and $\ln 1 = 0$ .

[F10]

Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm: For positive $x, y$ , $\ln (x y) = \ln x + \ln y$ , $\ln (x / y) = \ln x - \ln y$ , and $\ln (1 / x) = - \ln x$ .

[F11]

Change of base and inversion of the positive-base real exponential: $\log_{2} (2^{u}) = u$ for every real $u$ .

[F12]

Ceilings give the least positive integer meeting a real threshold: $⌈ x ⌉ = - ⌊ - x ⌋$ is an integer and $x \leq ⌈ x ⌉$ .

[F13]

Integer part: for every real $x$ there is exactly one integer $m$ with $m \leq x < m + 1$ : For every real $y$ , $⌊ y ⌋ \leq y < ⌊ y ⌋ + 1$ .

Proof

1.1F3F4givenconstruct

Let $C$ be uniquely decodable and set $K : = \sum_{i} 2^{- ℓ_{i}} > 0$ . By [F3] and [F4], $K \leq 1$ . Define $q_{i} : = 2^{- ℓ_{i}} / K$ ; then $q$ is a positive probability vector.

1.2F1F6F8F9F11F12givenconstructalgebra

Suppose $m \geq 2$ . Full support gives $0 < p_{i} < 1$ , so [F8] and [F9] give $- \log_{2} p_{i} > 0$ . By [F12], $ℓ_{i} = ⌈ - \log_{2} p_{i} ⌉$ is a positive integer and $ℓ_{i} \geq - \log_{2} p_{i}$ . Thus $\log_{2} (2^{- ℓ_{i}}) = - ℓ_{i} \leq \log_{2} p_{i}$ by [F11]; since $\log_{2}$ is strictly increasing by [F8] and [F9], this gives $2^{- ℓ_{i}} \leq p_{i}$ and hence $\sum_{i} 2^{- ℓ_{i}} \leq 1$ . By [F6] there is a binary prefix code with these lengths.

2.1F2F3F5F7F8F9F10step 1.1givenalgebra

By [F2], [F3], [F5], [F7], [F8], and [F10], using the logarithm product and quotient laws for the integer powers in $q_{i}$ , $0 \leq D (p ∥ q) = \sum_{i} p_{i} \ln (p_{i} / q_{i}) = - H (p) + (\ln 2) L_{p} (C) + \ln K$ . Since $K \leq 1$ , [F9] gives $\ln K \leq 0$ , so $H (p) \leq (\ln 2) L_{p} (C) + \ln K \leq (\ln 2) L_{p} (C)$ . Divide by $\ln 2 > 0$ from [F8] and use [F2] to obtain $H_{2} (p) \leq L_{p} (C)$ .

3.1F1F2F8F9F12F13step 1.2givenalgebra∎

By [F12] and [F13], if $m_{a} = ⌊ - a ⌋$ then $m_{a} \leq - a < m_{a} + 1$ , so $a \leq - m_{a} = ⌈ a ⌉ < a + 1$ . Therefore the Shannon code in step 1.2 satisfies $L_{p} (C) = \sum_{i} p_{i} ⌈ - \log_{2} p_{i} ⌉ < \sum_{i} p_{i} (- \log_{2} p_{i} + 1) = H_{2} (p) + 1$ . If $m = 1$ , then $p_{1} = 1$ by [F1], so $H_{2} (p) = 0$ by [F2] and [F8]–[F9]; the codeword $0$ is a prefix code of length one.

Depends on

Used by

Huffman expected length is within one bit of entropy Corollary

Dependency tree · two levels

42 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Stanford EE376A, Information Theory Course Notes, Chapter 4: Lossless Compression (standard reference, not scraped)
MIT OpenCourseWare 6.450, Memory-less sources, prefix free codes, and entropy (standard reference, not scraped)