Channel and question
- Input
- A finite common channel input \(X\).
- Output
- Finite receiver outputs \(Y_1\) and \(Y_2\).
- Law
- Receiver 1 is less noisy than receiver 2 when \(I(U;Y_1)\ge I(U;Y_2)\) for every finite \(U-X-(Y_1,Y_2)\).
- Quantity
- Private-message capacity region \(\mathcal C_{\mathrm{LN}}\), 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
| Result | Relation | Method | Year |
|---|---|---|---|
| Exact | \(\mathcal C_{\mathrm{LN}}=\mathcal R_{\mathrm{superposition}}\) | Superposition coding and a less-noisy converse. | 1979 |
Lean formalization
Version 1 · Lean. Less noisy is defined by auxiliary-variable dominance, separately from more capable.
CapacityAtlas.Channel.lessNoisyBroadcastCapacityStatementstatement
lean/CapacityAtlas/Channels/Broadcast.lean — Less-noisy capacity region equals the superposition region.
No external Lean proof is registered. Proofs longer than roughly 50 lines or requiring problem-specific infrastructure should live in a dedicated repository and link back to this statement version.
References
- Abbas El Gamal (1979). The Capacity of a Class of Broadcast Channels. IEEE Transactions on Information Theory. DOI 10.1109/TIT.1979.1056014.
Discussion
Thread key: capacityatlas:less-noisy-broadcast-channel