Channel and question
- Input
- One deterministic encoder maps a uniform common message to a word over a finite nonempty alphabet \(\mathcal X\).
- Output
- Each receiver \(j\) in a fixed finite nonempty set \(\mathcal J\) observes a word over its own finite nonempty alphabet \(\mathcal Y_j\).
- Law
- A memoryless joint law \(W((y_j)_{j\in\mathcal J}\mid x)\) governs each use. Receiver \(j\)'s marginal channel is \(W_j(y_j\mid x)\).
- Quantity
- Common-message broadcast capacity \(C_{\mathrm{common}}\), measured in bits per channel use.
Criterion. The supremum of rates supported at every sufficiently large blocklength with vanishing average decoding error at every receiver.
- Every receiver decodes the same message using only its own output word and its own deterministic decoder.
- Receiver outputs may be correlated within a use; the joint channel is memoryless across uses.
- The receiver set is fixed and does not grow with blocklength.
- There is no feedback, receiver cooperation, or input-cost constraint.
Current status
One input distribution serves every receiver; the finite minimum is attained, and compactness gives a maximizing input. Cover's Section III (pages 4–5) specifies the common-message model and finite-receiver extension; Section IX, equation (49), discusses the max–min formula through compound-channel results. The formal proof uses an exact reduction to the finite compound channel.
| Result | Relation | Method | Year |
|---|---|---|---|
| Lower | \(C_{\mathrm{common}}\ge\max_{P_X}\min_j I(X;Y_j)\) | A common code reliable over every receiver marginal, via the compound-channel coding theorem; Cover's Section IX, equation (49). | 1972 |
| Upper | \(C_{\mathrm{common}}\le\max_{P_X}\min_j I(X;Y_j)\) | The compound-channel converse uses one common input distribution to bound every receiver; the max–min characterization is discussed in Cover's Section IX, equation (49). | 1972 |
Formal verification
The locally proved canonical claim exposes the joint physical channel and receiver marginals. The proof tags receiver outputs and extends the decoder family to one compound decoder, preserving rates and receiver errors exactly, then applies the local compound-channel capacity theorem. Both proofs are included in this repository's build and transitive axiom audit. This is the formal proof route, not an attributed historical construction.
Claims
- The operational common-message capacity of any finite joint broadcast channel equals the max–min of its receiver mutual informations over one shared input distribution.
exact-capacity· exact capacity · solved · Formally proved · v1
Lean declarations (6)
CapacityAtlas.CommonMessageBroadcast.BlockCodeAPI
lean/CapacityAtlasForMathlib/InformationTheory/CommonMessageBroadcast.lean — One message encoder and a decoder for each receiver's own output alphabet.CapacityAtlas.CommonMessageBroadcast.receiverChannelsAPI
lean/CapacityAtlasForMathlib/InformationTheory/CommonMessageBroadcast.lean — Receiver marginals of an arbitrary memoryless joint broadcast law.CapacityAtlas.CommonMessageBroadcast.operationalCapacityBitsAPI
lean/CapacityAtlasForMathlib/InformationTheory/CommonMessageBroadcast.lean — Common-message average-error capacity at all sufficiently large blocklengths.CapacityAtlas.CommonMessageBroadcast.informationCapacityBitsAPI
lean/CapacityAtlasForMathlib/InformationTheory/CommonMessageBroadcastInformation.lean — The max–min information target for receiver-dependent output alphabets.CapacityAtlas.CommonMessageBroadcast.exists_capacityAchieving_inputAPI
lean/CapacityAtlasForMathlib/InformationTheory/CommonMessageBroadcastInformation.lean — A common input distribution attains the max–min information target.CapacityAtlas.Channel.commonMessageBroadcastCapacityStatementclaim · exact-capacity
lean/CapacityAtlas/Channels/CommonMessageBroadcast.lean — Locally proved joint-channel common-message capacity theorem.
References
- Thomas M. Cover (1972). Broadcast Channels. IEEE Transactions on Information Theory 18(1), 2–14. DOI 10.1109/TIT.1972.1054727.
- 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.