CCapacity Atlas
causal-state-information-channel

DMC with causal state information at the encoder

An iid channel state is revealed causally to the encoder but not to the decoder.

Point-to-point Finite alphabet Discrete memoryless Causal state information Side information Capacity Exact Single-letter characterization

Channel and question

Input
A symbol \(X_t\in\mathcal X\), chosen as \(X_t=f_t(M,S^t)\), with a finite nonempty alphabet.
Output
The decoder observes only \(Y^n\), with finite nonempty output alphabet \(\mathcal Y\).
Law
The finite state alphabet has law q; conditioned on input and state sequences, outputs are independent with transition \(W(y_t\mid x_t,s_t)\).
Quantity
Shannon-strategy capacity \(C_{\mathrm{causal}}\), 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.

  • States are iid, independent of the message, and revealed to the encoder before choosing the current input.
  • The encoder may use all past and current states, but no future states and no output feedback.
  • The decoder does not know the state sequence; both terminals know the state distribution and channel law.
  • Encoders and decoders are deterministic, messages are uniform, and average decoding error vanishes.
  • There is no input-cost constraint.

Current status

\[C_{\mathrm{causal}}=\max_{P_U,\,x=f(U,S),\,U\perp S} I(U;Y)\]

Equivalently, maximize over distributions on the fixed finite alphabet of functions from states to inputs. The induced strategy channel averages W(y|t(s),s) over q(s). Shannon's unnumbered theorem gives this capacity equivalence; ordinary strategy codes form a subclass of all causal codes.

Known results and bounds for DMC with causal state information at the encoder
ResultRelationMethodYear
Lower\(C_{\mathrm{causal}}\ge\max_{P_U,\,x=f(U,S),\,U\perp S} I(U;Y)\)Embed ordinary DMC codes on the finite strategy alphabet by evaluating each strategy at the current state.1958
Upper\(C_{\mathrm{causal}}\le\max_{P_U,\,x=f(U,S),\,U\perp S} I(U;Y)\)Message and past states determine the current strategy; a conditional-entropy bound and Fano inequality bound all history-dependent causal codes.1958

Formal verification

Lean coverageFormally stated

The local proof embeds strategy codes and bounds arbitrary causal policies using entropy and Fano’s inequality. It also proves that an optimizing strategy distribution exists.

Claims

  • Operational capacity of arbitrary deterministic causal-state codes equals the information capacity of the finite Shannon-strategy channel.
    exact-capacity · exact capacity · solved · Formally proved · v1
Lean declarations (6)
Linked proofs (1)
  • exact-capacity · complete · claim v1
    TomasOrtega/CapacityAtlasCausalState@0176a0e9 · CapacityAtlasCausal.capacityCertificate
    Historical upstream certificate imported into this repository. The upstream proof pins Atlas commit 661affbfb9241fcc2b926db78564d81731a42f14 and audits every transitive proof axiom and exact canonical-proposition correspondence.

References

  1. Claude E. Shannon (1958). Channels with Side Information at the Transmitter. IBM Journal of Research and Development. DOI 10.1147/rd.24.0289.
  2. Abbas El Gamal and Young-Han Kim (2011). Network Information Theory. Cambridge University Press. DOI 10.1017/CBO9781139030687.

Discussion

Find discussionStart discussion

Related problems

Binary Z-channel Z-channel

One binary symbol is transmitted perfectly while the other can flip in only one direction.

Point-to-point Binary Finite alphabet Discrete memoryless Asymmetric Capacity Exact
Solved \(C_Z(p)=\log_2\!\left(1+(1-p)p^{p/(1-p)}\right)\)
Binary erasure channel BEC

Each transmitted bit is received correctly or replaced by a visible erasure symbol.

Point-to-point Binary Finite alphabet Discrete memoryless Symmetric Erasure Capacity Exact
Solved \(C_{\mathrm{BEC}}(\varepsilon)=1-\varepsilon\)
Binary memory with encoder-known stuck-at defects

Independent stuck-at defects are known noncausally to the encoder but not the decoder.

Point-to-point Binary Finite alphabet Discrete memoryless Noncausal state information Capacity Exact
Solved \(C=1-\delta\)
Binary symmetric channel BSC

Each bit is independently flipped with probability \(p\).

Point-to-point Binary Finite alphabet Discrete memoryless Symmetric Capacity Exact
Solved \(C_{\mathrm{BSC}}(p)=1-h_2(p)\)