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
\[C_{\mathrm{common}}=\max_{P_X}\min_{j\in\mathcal J}I(X;Y_j)\]
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
Lean coverageFormally stated
The canonical proposition exposes the joint physical channel and receiver marginals. The formal proof tags receiver outputs and extends the decoder family to one compound decoder, preserving rates and receiver errors exactly. 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 — Canonical joint-channel common-message capacity proposition.
Linked proofs (1)
- exact-capacity · complete · claim v1
TomasOrtega/CapacityAtlasCommonMessage@83923a9a·CapacityAtlasCommonMessage.capacityCertificate
Pins Atlas 1f4b83da5f2bc05efba649054be18b1f6fd8da31 and compound proof 1d5cbdc0a8cfb5d034facdb8d1e2473bb3c40ebe. The imported proof is rebuilt against the resolved Atlas prerequisite. The audit checks transitive axioms and full canonical-proposition correspondence with rigid universes; negative controls reject a different proposition and a universe-restricted certificate.
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.