Channel and question
- Input
- At time \(t\), the encoder chooses \(X_t\) from the message and \(Y^{t-1}\).
- Output
- \(Y_t\) is fed back noiselessly after each use.
- Law
- \(W(y_t|x_t)\) is memoryless in the forward direction.
- Quantity
- Feedback capacity \(C_{\mathrm{fb}}(W)\), measured in bits per channel use.
Criterion. Average-error capacity with causal feedback.
- Feedback is causal, noiseless, and unlimited.
- The criterion is vanishing average error, not zero error.
Current status
\[C_{\mathrm{fb}}(W)=C(W)=\max_{P_X}I(X;Y)\]
| Result | Relation | Method | Year |
|---|---|---|---|
| Lower | \(C_{\mathrm{fb}}\ge C\) | Use any capacity-achieving no-feedback code. | 1956 |
| Upper | \(C_{\mathrm{fb}}\le\max_{P_X}I(X;Y)\) | Directed dependence through feedback does not exceed the per-use mutual-information maximum for a memoryless channel. | 1956 |
Lean formalization
Canonical statementNone
Version 1 · Lean. Causal feedback encoders and block codes are not yet in the Lean API.
Substantial proofs0 linked
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
- Claude E. Shannon (1956). The Zero Error Capacity of a Noisy Channel. IRE Transactions on Information Theory. DOI 10.1109/TIT.1956.1056798.
- Thomas M. Cover and Joy A. Thomas (2006). Elements of Information Theory. Wiley, second edition. DOI 10.1002/047174882X.
Discussion
Thread key: capacityatlas:discrete-memoryless-channel-with-feedback