Channel and question
- Input
- \(X\in\mathbb R\), with average power \(P\).
- Output
- \(Y=X+S+Z\).
- Law
- Gaussian state \(S\) is known noncausally to the encoder; \(Z\sim\mathcal N(0,N)\) is independent.
- Quantity
- Dirty-paper capacity \(C_{\mathrm{DPC}}\), measured in bits per channel use.
Criterion. Average-error capacity. Resource averaging is fixed by the explicit model assumption below.
- The decoder does not know S.
- State and noise are iid Gaussian.
- For every message m, E_{S^n}[sum_t x_t(m,S^n)^2] <= n P. Energy is integrable under the iid state law. The bound is not pathwise in the state and is not averaged over messages.
Current status
\[C_{\mathrm{DPC}}=\frac12\log_2\!\left(1+\frac PN\right)\]
The value is independent of the state variance.
| Result | Relation | Method | Year |
|---|---|---|---|
| Lower | \(C_{\mathrm{DPC}}\ge\frac12\log_2(1+P/N)\) | Gaussian Gel'fand-Pinsker coding pre-cancels the known interference. | 1983 |
| Upper | \(C_{\mathrm{DPC}}\le\frac12\log_2(1+P/N)\) | Reveal the interference to the decoder and apply the AWGN converse. | 1983 |
Formal verification
Lean coverageFormally stated
Concrete operational definitions and admitted research statements are present. Existing proofs are preserved. New statements require mathematical review and proof completion. Power convention: PerMessageStateAveragePowerAdmissible. No equivalence to another power convention is assumed.
Claims
- Noncausal independent Gaussian interference at the encoder causes no capacity loss.
operational-capacity· exact capacity · solved · Formally stated · v1
Lean declarations (1)
CapacityAtlas.Claims.dirtyPaperclaim · operational-capacity
lean/CapacityAtlas/Claims/DirtyPaper.lean — Noncausal independent Gaussian interference at the encoder causes no capacity loss.
References
- Max H. M. Costa (1983). Writing on Dirty Paper. IEEE Transactions on Information Theory. DOI 10.1109/TIT.1983.1056659.