Shannon's source coding theorem

The statement fixes a finite, nonempty index type $\iota$ (the "source alphabet," with $|\iota|\ge 1$) and a function $p:\iota\to\mathbb{R}$ together with two hypotheses on it: hp_pos asserts $p_i>0$ for every $i\in\iota$ (strict positivity at every index, no zero-probability symbols allowed), and hp_sum asserts $\sum_{i\in\iota}p_i=1$ (so $p$ is a genuine probability distribution on $\iota$, and since it is strictly positive and sums to $1$, necessarily $0<p_i\le 1$ for each $i$). It also fixes a second finite, nonempty type $\alpha$ (the "code alphabet") subject to hD: $\operatorname{Fintype.card}\alpha \ge 2$, i.e. the code alphabet has at least two symbols. The quantity entropy p (Fintype.card α) unfolds by definition to $H := -\sum_{i\in\iota} p_i \cdot \log_{|\alpha|}(p_i)$, where $|\alpha|=\operatorname{Fintype.card}\alpha$ is used as the (real, $\ge 2$) base of Real.logb. The predicate InformationTheory.UniquelyDecodable(S) for a set $S\subseteq \mathrm{List}\,\alpha$ unfolds to: for all finite lists of lists $L_1, L_2 : \mathrm{List}(\mathrm{List}\,\alpha)$, if every element (word) of $L_1$ lies in $S$ and every element of $L_2$ lies in $S$, and the flattening/concatenation of $L_1$ equals the flattening/concatenation of $L_2$ (as a single list over $\alpha$), then $L_1=L_2$ as lists — i.e. two finite sequences of words drawn from $S$ that concatenate to the same string of symbols must be the identical sequence of words (same length, same words in the same order). With these unfoldings, the theorem's conclusion is a conjunction of two separate claims about functions $c:\iota\to\mathrm{List}\,\alpha$ (assigning to each source symbol $i$ a "codeword," a finite — possibly empty, since no minimum length is imposed — string over $\alpha$, of length $(c\,i).\mathrm{length}$), and the two claims use independently quantified $c$'s, not a shared one. The first conjunct is universally quantified: for every $c:\iota\to\mathrm{List}\,\alpha$ such that $c$ is injective (distinct source symbols get distinct codewords) and $\mathrm{Set.range}\,c=\{c\,i : i\in\iota\}$ (the set of codewords actually used, as a set, without multiplicity) is uniquely decodable in the sense just unfolded, it holds that $H \le \sum_{i\in\iota} p_i\cdot (c\,i).\mathrm{length}$ — the entropy (base $|\alpha|$) is a lower bound on the $p$-weighted average codeword length, for every such injective, uniquely-decodable-range code. The second conjunct is existentially quantified with a separately-chosen $c$ (not required to be related to the $c$'s ranging over the first conjunct): there exists $c:\iota\to\mathrm{List}\,\alpha$ that is injective, whose range $\mathrm{Set.range}\,c$ is uniquely decodable (same unfolded meaning), and for which the $p$-weighted average codeword length is strictly less than $H+1$, i.e. $\sum_{i\in\iota}p_i\cdot(c\,i).\mathrm{length} < H+1$. Both conjuncts together assert the ≤-bound holding for all injective, uniquely-decodable codes and the existence of one particular such code achieving strictly less than $H+1$; note also that since $|\iota|\ge1$, $|\alpha|\ge2$, and every $p_i\in(0,1]$, the sum defining $H$ and each Real.logb evaluation are over strictly positive arguments with a well-defined base $\ge 2$, so no vacuous-sum or log-of-nonpositive/log-base-degenerate cases arise from the stated hypotheses, though the case $|\iota|=1$ is permitted (forcing $p\equiv 1$ and $H=0$), as is the use of the empty list ($(c\,i).\mathrm{length}=0$) as a codeword since $c$'s codomain is unrestricted $\mathrm{List}\,\alpha$.