Shannon's source coding theorem, corrected

Read‑back.

The bundle first fixes two auxiliary definitions and then states a theorem about them.

Entropy. For a finite index type $\iota$ with a Fintype instance, a function $p:\iota\to\mathbb R$, and a natural number $D$, entropy p D is defined as $-\sum_{i\in\iota} p_i\cdot \log_D(p_i)$, where $\log_D$ is Real.logb D, i.e. $\log_D(x)=\dfrac{\ln x}{\ln D}$ with $D$ coerced from $\mathbb N$ to $\mathbb R$. No hypothesis is built into this definition itself (e.g. it does not require $p_i>0$ or $D\ge 2$); it is a bare real-valued formula, applied at zero or on non‑positive/degenerate $p_i,D$ it would just evaluate the formula literally (with the usual Lean/Mathlib conventions for $\log$ of a non‑positive argument or $\log_D$ with $D\le 1$).

Unique decodability. For a type $\alpha$ and a set $S\subseteq \mathrm{List}\,\alpha$ of "codewords", InformationTheory.UniquelyDecodable S says: for every pair of lists-of-lists $L_1, L_2 : \mathrm{List}(\mathrm{List}\,\alpha)$ such that every element $w$ occurring in $L_1$ lies in $S$ and every element $w$ occurring in $L_2$ lies in $S$, if the concatenation (flatten) of $L_1$ equals the concatenation of $L_2$ as a single list of $\alpha$'s, then $L_1=L_2$ as lists (same codewords, in the same order, same length). Equivalently: the concatenation map, restricted to finite sequences drawn from $S$, is injective.

Theorem shannon_source_coding_theorem_v2. The hypotheses are: $\iota$ is a type with a Fintype instance and a Nonempty instance; $p:\iota\to\mathbb R$; hp_pos asserts $0<p_i$ for every $i\in\iota$ (strict positivity at every index, no index may have $p_i=0$); hp_sum asserts $\sum_{i\in\iota} p_i = 1$ exactly; hι asserts $2\le \mathrm{card}(\iota)$, i.e. the index/source alphabet has at least two elements — this is a hypothesis in addition to the Nonempty ι instance and is strictly stronger than it (so Nonempty ι is logically redundant given hι, though both appear as separate premises in the signature). Separately, $\alpha$ is a type with Fintype and Nonempty instances, and hD asserts $2\le \mathrm{card}(\alpha)$ (the target/code alphabet also has at least two elements; again Nonempty α is redundant given hD). With $H := \mathrm{entropy}\,p\,(\mathrm{card}\,\alpha) = -\sum_{i\in\iota} p_i\log_{\mathrm{card}(\alpha)}(p_i)$, the conclusion is a conjunction of two separate statements, each quantifying its own, independently-chosen function $c$ — the $c$ bound in the first conjunct is not the same as, nor tied to, the $c$ bound in the second:

1. (Universal / lower-bound clause) For every $c:\iota\to \mathrm{List}\,\alpha$ that is injective (Function.Injective c, i.e. $c(i)=c(j)\Rightarrow i=j$) and whose range $\{c(i): i\in\iota\}$ is uniquely decodable in the sense above, it holds that $H \le \sum_{i\in\iota} p_i\cdot |c(i)|$ (a non-strict inequality; $|c(i)|$ is the length of the list $c(i)$).

2. (Existential / near-achievability clause) There exists a $c:\iota\to\mathrm{List}\,\alpha$ that is injective and whose range is uniquely decodable, and for this particular $c$, $\sum_{i\in\iota} p_i\cdot |c(i)| < H+1$ (a strict inequality).

The two clauses are joined by ∧ at the top level of the theorem's statement, so the theorem asserts both (1) and (2) hold simultaneously; nothing links the witness $c$ of clause (2) to the universally-quantified $c$'s of clause (1) beyond each independently satisfying injectivity and unique decodability of its range.