Point-to-point
Updated 2026-08-09
Binary symmetric channel
Solved
Lean: definitions
Each bit is independently flipped with probability p. This is the canonical finite noisy channel.
Multi-user
Physically degraded two-receiver broadcast channel
One transmitter sends private messages to two receivers whose outputs form a degradation chain.
Solved
Lean: not started
01 · Model
Channel specification
Input
\(X\in\mathcal X\)
Output
Receiver outputs \(Y_1\) and \(Y_2\).
Law
A memoryless channel satisfying \(X\to Y_1\to Y_2\).
Assumptions
- Receiver 1 is the stronger receiver.
- Each receiver requests its own private message.
02 · Capacity
Capacity region
rate pairs in bits per channel use
region
\[\mathcal C=\bigcup_{p(u,x)}\{(R_1,R_2):R_1\le I(X;Y_1\mid U),\ R_2\le I(U;Y_2)\}\]
Conditions. \(U\to X\to Y_1\to Y_2\).
03 · Evidence
Known bounds and characterizations
04 · History
Bound timeline
-
1973
Bergmans proved the capacity region for degraded broadcast channels.
Reference
05 · Lean
Formalization status
Lean: not started
Not started
Multi-user rate regions and auxiliary random variables are not yet formalized.
- Definitions
- Statement
- Partial proof
- Complete proof
No Lean file is linked yet. A contribution should begin by reusing the shared definitions under lean/CapacityAtlas.
References
Primary sources
- (1973). Random coding theorem for broadcast channels with degraded components. IEEE Transactions on Information Theory. doi:10.1109/TIT.1973.1054980
- (2006). Elements of Information Theory. Wiley, second edition. doi:10.1002/047174882X
Keep exploring
Related entries
Multi-user
Updated 2026-08-09
General discrete memoryless relay channel
Open
Lean: not started
A relay assists communication from a source to a destination. Decode-forward and the cut-set bound do not coincide in general.
Point-to-point
Updated 2026-08-09
Binary erasure channel
Solved
Lean: definitions
Each transmitted bit is either received correctly or replaced by a visible erasure symbol.