Channel and question
- Input
- One of three symbols \(x\in\{0,1,2\}\).
- Output
- Two binary outputs with pairs \((Y_1,Y_2)=(0,0),(0,1),(1,1)\), respectively.
- Law
- Both receiver outputs are deterministic functions of the input.
- Quantity
- Private-message capacity region \(\mathcal C_{\mathrm B}\), measured in ordered pairs of bits per channel use.
Criterion. Closure of achievable nonnegative private-message rate pairs.
- Independent private messages are sent to the two receivers.
- Average probability that either receiver errs vanishes.
Current status
\[R_1\le H(Y_1),\quad R_2\le H(Y_2),\quad R_1+R_2\le H(Y_1,Y_2)\]
Conditions. Union over all input distributions on the three symbols.
| Result | Relation | Method | Year |
|---|---|---|---|
| Exact | \(\mathcal C_{\mathrm B}=\bigcup_{P_X}\{R_1\le H(Y_1),R_2\le H(Y_2),R_1+R_2\le H(Y_1,Y_2)\}\) | Deterministic broadcast coding theorem. | 1980 |
Formal verification
Lean coverageFormally stated
New statements await mathematical review and proofs.
Claims
- The operational private-message region of the registered Blackwell channel.
operational-capacity· exact capacity · solved · Formally stated · v1
Lean declarations (3)
CapacityAtlas.Channel.blackwellBroadcastChanneldefinition
lean/CapacityAtlas/Channels/Broadcast.lean — Concrete deterministic Blackwell broadcast channel.CapacityAtlas.Channel.blackwellCapacityRegiondefinition
lean/CapacityAtlas/Channels/Broadcast.lean — Deterministic single-letter private-message region.CapacityAtlas.Claims.blackwellclaim · operational-capacity
lean/CapacityAtlas/Claims/Blackwell.lean — The operational private-message region of the registered Blackwell channel.
References
- Sergei I. Gel'fand and Mark S. Pinsker (1980). Capacity of a Broadcast Channel with One Deterministic Component. Problems of Information Transmission.