Channel and question
- Input
- A word over a finite nonempty alphabet \(\mathcal X\), determined by the message alone.
- Output
- A word over a common finite nonempty output alphabet \(\mathcal Y\).
- Law
- A fixed unknown member \(W_s(y|x)\) of a known finite nonempty family governs every use, with conditionally independent outputs.
- Quantity
- Compound-channel capacity \(C_{\mathrm{cmp}}\), measured in bits per channel use.
Criterion. The supremum of rates supported at every sufficiently large blocklength with uniformly vanishing average error over the channel family.
- The same member s applies throughout the block; neither encoder nor decoder knows s.
- One deterministic encoder and one deterministic decoder must work for every family member.
- Messages are uniform, and their average decoding error must vanish uniformly over the family.
- There is no feedback and no input-cost constraint.
Current status
\[C_{\mathrm{cmp}}=\max_{P_X}\min_{s\in\mathcal S} I(P_X,W_s)\]
The finite minimum is attained, and compactness of the input simplex gives a maximizing input. Lapidoth and Telatar state the compound DMC formula in equation (1), with the channel-independent decoder convention on page 973 and the uniform average-error criterion in Definition 1.
| Result | Relation | Method | Year |
|---|---|---|---|
| Lower | \(C_{\mathrm{cmp}}\ge\max_{P_X}\min_s I(P_X,W_s)\) | A common codebook and channel-independent decoder achieve the worst mutual information for a chosen input law. | 1959 |
| Upper | \(C_{\mathrm{cmp}}\le\max_{P_X}\min_s I(P_X,W_s)\) | Fano's inequality, entropy subadditivity, and mutual-information concavity give one averaged input distribution satisfying every member's rate bound. | 1959 |
Formal verification
Lean coverageFormally stated
The local proof uses a common decoder for a uniform mixture of whole-block channels. The converse keeps one averaged input distribution across the family. The proof also establishes that the max–min is attained.
Claims
- Operational capacity with one common encoder and decoder equals the maximum, over input distributions, of the least mutual information across the finite channel family.
exact-capacity· exact capacity · solved · Formally proved · v1
Lean declarations (5)
CapacityAtlas.CompoundChannel.BlockCodeAPI
lean/CapacityAtlasForMathlib/InformationTheory/CompoundChannel.lean — One deterministic encoder and decoder independent of the unknown member.CapacityAtlas.CompoundChannel.operationalCapacityBitsAPI
lean/CapacityAtlasForMathlib/InformationTheory/CompoundChannel.lean — Uniform average-error capacity at all sufficiently large blocklengths.CapacityAtlas.CompoundChannel.informationCapacityBitsAPI
lean/CapacityAtlasForMathlib/InformationTheory/CompoundChannel.lean — Supremum over input distributions of the least member mutual information.CapacityAtlas.CompoundChannel.exists_capacityAchieving_inputAPI
lean/CapacityAtlasForMathlib/InformationTheory/CompoundChannel.lean — An input distribution attains the max–min information target.CapacityAtlas.Channel.compoundCapacityStatementclaim · exact-capacity
lean/CapacityAtlas/Channels/Compound.lean — Canonical finite compound-channel capacity proposition.
Linked proofs (1)
- exact-capacity · complete · claim v1
TomasOrtega/CapacityAtlasCompound@1d5cbdc0·CapacityAtlasCompound.capacityCertificate
Historical upstream certificate imported into this repository. Pins Atlas commit 61a109e8cba1b8afa4b42c68afd96a3df71120d0. The upstream audit checks every transitive proof axiom and exact canonical-proposition correspondence with rigid universes; negative controls reject a different proposition and a universe-restricted certificate.
References
- David Blackwell, Leo Breiman, and A. J. Thomasian (1959). The Capacity of a Class of Channels. Annals of Mathematical Statistics. DOI 10.1214/aoms/1177706106.
- Amos Lapidoth and İ. Emre Telatar (1998). The Compound Channel Capacity of a Class of Finite-State Channels. IEEE Transactions on Information Theory.
- Thomas M. Cover and Joy A. Thomas (2006). Elements of Information Theory. Wiley, second edition. DOI 10.1002/047174882X.