Channel and question
- Input
- A symbol \(X\in\mathcal X\), with a finite nonempty input alphabet.
- Output
- The decoder observes both \(Y\in\mathcal Y\) and \(S\in\mathcal S\), with finite nonempty alphabets.
- Law
- The state has fixed law \(q(s)\), and \(P(S=s,Y=y\mid X=x)=q(s)W(y\mid x,s)\).
- Quantity
- Decoder-state capacity \(C_{\mathrm{SI-D}}\), measured in bits per channel use.
Criterion. The supremum of rates supported at every sufficiently large blocklength with vanishing average error over messages, states, and channel outputs.
- The state sequence is independent and identically distributed and independent of the message.
- The encoder knows the laws q and W but observes no state information and receives no feedback.
- The decoder knows the entire state and output sequences when decoding the block.
- Encoders and decoders are deterministic, messages are uniform, and average decoding error vanishes.
- There is no input-cost constraint.
Current status
\[C_{\mathrm{SI-D}}=\max_{P_X} I(X;Y\mid S)\]
The maximization uses one input law independent of the state. Heegard and El Gamal's Theorem 2(d), with zero encoder state-description rate, gives this formula; Section III uses the paired output (S,Y).
| Result | Relation | Method | Year |
|---|---|---|---|
| Lower | \(C_{\mathrm{SI-D}}\ge\max_{P_X}I(X;Y\mid S)\) | Apply finite-DMC random coding with the state and physical output treated jointly as the receiver observation. | 1983 |
| Upper | \(C_{\mathrm{SI-D}}\le\max_{P_X}I(X;Y\mid S)\) | Apply the finite-DMC converse to the paired output and use independence of input and state. | 1983 |
Formal verification
Lean coverageFormally stated
The paired-output channel has exactly the iid-state block law. A finite entropy identity equates its mutual information with the state average, including zero-probability states. The local capacity proof reuses the finite-DMC coding theorem; compactness supplies an optimizing input.
Claims
- Operational average-error capacity equals the supremum of state-averaged mutual information over input laws independent of the state.
exact-capacity· exact capacity · solved · Formally proved · v1 - One input distribution independent of the state attains the operational capacity.
optimizing-input· structural · solved · Formally proved · v1
Lean declarations (6)
CapacityAtlas.Channel.decoderStateChanneldefinition
lean/CapacityAtlas/Channels/DecoderState.lean — State-dependent DMC with the state included in the decoder observation.CapacityAtlas.Channel.decoderStateInformationCapacityBitsdefinition
lean/CapacityAtlas/Channels/DecoderState.lean — Supremum of conditional mutual information over a single state-independent input law.CapacityAtlas.Channel.decoderState_operationalCapacityclaim · exact-capacity
lean/CapacityAtlas/Channels/DecoderState.lean — Exact operational capacity by reduction to the paired-output finite DMC.CapacityAtlas.Channel.decoderState_capacityAchieving_inputclaim · optimizing-input
lean/CapacityAtlas/Channels/DecoderState.lean — A single input law attains the capacity for the prescribed state distribution.CapacityAtlas.FiniteChannel.withDecoderState_block_transitionAPI
lean/CapacityAtlasForMathlib/InformationTheory/DecoderSideInformation.lean — The block transition factors into the iid state mass and the conditional memoryless channel law.CapacityAtlas.FiniteChannel.withDecoderState_mutualInformationBitsAPI
lean/CapacityAtlasForMathlib/InformationTheory/DecoderSideInformation.lean — Mutual information of the paired-output channel equals the state average of per-state mutual information.
References
- Chris Heegard and Abbas A. El Gamal (1983). On the Capacity of Computer Memory with Defects. IEEE Transactions on Information Theory.
- Claude E. Shannon (1948). A Mathematical Theory of Communication. Bell System Technical Journal. DOI 10.1002/j.1538-7305.1948.tb01338.x.