Channel and question
- Input
- Independent finite-alphabet inputs \(X_1\) and \(X_2\).
- Output
- Finite receiver outputs \(Y_1\) and \(Y_2\).
- Law
- A memoryless two-user interference channel satisfying the strong-interference inequalities for every product input law.
- Quantity
- Strong-interference capacity region \(\mathcal C_{\mathrm{SI}}\), measured in ordered pairs of bits per channel use.
Criterion. Closure of achievable independent-message rate pairs.
- Transmitters carry independent private messages.
- Average probability that either receiver errs vanishes.
Current status
Conditions. The strong-interference inequalities hold for every product input distribution.
| Result | Relation | Method | Year |
|---|---|---|---|
| Exact | \(\mathcal C_{\mathrm{SI}}=\mathcal C_{\mathrm{MAC},1}\cap\mathcal C_{\mathrm{MAC},2}\) | Both receivers decode both messages without a rate penalty. | 1975 |
Formal verification
New statements await mathematical review and proofs.
Claims
- The strong-interference region uses the same time-sharing law at both receivers.
operational-capacity· exact capacity · solved · Formally stated · v1
Lean declarations (3)
CapacityAtlas.FiniteInterferenceChanneldefinition
lean/CapacityAtlasForMathlib/Network/FiniteInterferenceChannel.lean — Concrete two-user finite interference channel.CapacityAtlas.FiniteInterferenceChannel.IsStrongInterferencedefinition
lean/CapacityAtlasForMathlib/Network/FiniteInterferenceChannel.lean — Strong-interference mutual-information conditions.CapacityAtlas.Claims.strongInterferenceclaim · operational-capacity
lean/CapacityAtlas/Claims/StrongInterference.lean — The strong-interference region uses the same time-sharing law at both receivers.
References
- A. B. Carleial (1975). A Case Where Interference Does Not Reduce Capacity. IEEE Transactions on Information Theory. DOI 10.1109/TIT.1975.1055352.
- Te Sun Han and Kingo Kobayashi (1981). A New Achievable Rate Region for the Interference Channel. IEEE Transactions on Information Theory. DOI 10.1109/TIT.1981.1056307.