Channel and question
- Input
- A finite common channel input \(X\).
- Output
- Finite receiver outputs \(Y_1\) and \(Y_2\).
- Law
- Receiver 1 is more capable when \(I(X;Y_1)\ge I(X;Y_2)\) for every input distribution.
- Quantity
- Private-message capacity region \(\mathcal C_{\mathrm{MC}}\), measured in ordered pairs of bits per channel use.
Criterion. Closure of achievable private-message rate pairs.
- Independent private messages and vanishing average error.
- Arbitrary finite superposition auxiliary alphabets are allowed.
Current status
\[\mathcal C_{\mathrm{MC}}=\bigcup_{P_U P_{X|U}}\{R_2\le I(U;Y_2),\ R_1+R_2\le\min[I(X;Y_1),I(X;Y_1\mid U)+I(U;Y_2)]\}\]
| Result | Relation | Method | Year |
|---|---|---|---|
| Exact | \(R_2\le I(U;Y_2),\quad R_1+R_2\le\min\{I(X;Y_1),I(X;Y_1\mid U)+I(U;Y_2)\}\) | Superposition coding and a more-capable converse. | 1979 |
Formal verification
Lean coverageFormally stated
New statements await mathematical review and proofs.
Claims
- The more-capable private-message region, including its sum-rate condition.
operational-capacity· exact capacity · solved · Formally stated · v1
Lean declarations (2)
CapacityAtlas.FiniteBroadcastChannel.IsMoreCapabledefinition
lean/CapacityAtlasForMathlib/InformationTheory/FiniteBroadcastChannel.lean — More-capable ordering for every input distribution.CapacityAtlas.Claims.moreCapableBroadcastclaim · operational-capacity
lean/CapacityAtlas/Claims/MoreCapableBroadcast.lean — The more-capable private-message region, including its sum-rate condition.
References
- Abbas El Gamal (1979). The Capacity of a Class of Broadcast Channels. IEEE Transactions on Information Theory. DOI 10.1109/TIT.1979.1056014.