Capacity Atlas Channel-capacity problems
Point-to-point

Finite discrete memoryless channel

The general finite memoryless point-to-point channel has a single-letter mutual-information characterization.

Solved Lean: definitions DMC
01 · Model

Channel specification

Input

\(X\in\mathcal X\), with finite \(\mathcal X\).

Output

\(Y\in\mathcal Y\), with finite \(\mathcal Y\).

Law

A stochastic matrix \(W(y\mid x)\), used independently at each channel use.

Assumptions

  • The channel law is known to encoder and decoder.
  • Average probability of error vanishes with blocklength.
02 · Capacity

Shannon capacity

bits per channel use characterization
\[C(W)=\max_{P_X} I(X;Y)\]

The maximum is over all probability distributions on the finite input alphabet.

Symbol
\(C(W)\)
Error criterion
Average-error capacity.
03 · Evidence

Known bounds and characterizations

TypeClaimMethodSource
lower \(C(W)\ge\max_{P_X}I(X;Y)\) Random coding and typical-set decoding. 1948 [1]
upper \(C(W)\le\max_{P_X}I(X;Y)\) Fano's inequality, the chain rule, and memorylessness. 1948 [1]
04 · History

Bound timeline

  1. 1948

    Shannon proved the noisy-channel coding theorem.

    Reference
05 · Lean

Formalization status

Lean: definitions

Definitions

Shared finite stochastic channels, serial composition, and one-shot codes are formalized. The asymptotic coding theorem is not.

  1. Definitions
  2. Statement
  3. Partial proof
  4. Complete proof
CapacityAtlas.FiniteChannel Shared finite stochastic-channel structure. lean/CapacityAtlas/FiniteChannel.lean CapacityAtlas.OneShotCode Shared one-shot encoder, decoder, and error definitions. lean/CapacityAtlas/Code.lean
References

Primary sources

  1. Claude E. Shannon (1948). A Mathematical Theory of Communication. Bell System Technical Journal. doi:10.1002/j.1538-7305.1948.tb01338.x
  2. Thomas M. Cover and Joy A. Thomas (2006). Elements of Information Theory. Wiley, second edition. doi:10.1002/047174882X
Keep exploring

Related entries

Point-to-point Updated 2026-08-09

Binary symmetric channel

Solved Lean: definitions

Each bit is independently flipped with probability p. This is the canonical finite noisy channel.

2 bounds Open entry