Capacity Atlas Channel-capacity problems
Point-to-point

Binary symmetric channel

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

Solved Lean: definitions BSC
01 · Model

Channel specification

Input

\(X\in\{0,1\}\)

Output

\(Y\in\{0,1\}\)

Law

Y=X\oplus Z, where Z\sim\mathrm{Bernoulli}(p) independently across uses.

Parameters

SymbolMeaningRange
\(p\) Crossover probability. \(0\le p\le1/2\)

Assumptions

  • The range p at most 1/2 removes the equivalent relabelled regime.
  • Average probability of error vanishes with blocklength.
02 · Capacity

Shannon capacity

bits per channel use exact
\[C_{\mathrm{BSC}}(p)=1-h_2(p)\]

Conditions. 0\le p\le1/2, where h_2 is binary entropy.

The uniform input distribution achieves capacity.

Symbol
\(C_{\mathrm{BSC}}(p)\)
Error criterion
Average-error capacity.
03 · Evidence

Known bounds and characterizations

TypeClaimMethodSource
lower \(C\ge1-h_2(p)\) Apply the noisy-channel coding theorem to independent uniform inputs. 1948 [1]
upper \(C\le1-h_2(p)\) Maximize I(X;Y) over the binary input distribution; symmetry makes the uniform input optimal. 1948 [1]
04 · History

Bound timeline

  1. 1948

    Shannon's noisy-channel coding theorem determines the capacity.

    Reference
05 · Lean

Formalization status

Lean: definitions

Definitions

The transition kernel and its zero-noise identity are formalized. The coding theorem and entropy optimization remain open.

  1. Definitions
  2. Statement
  3. Partial proof
  4. Complete proof
CapacityAtlas.Channel.binarySymmetric Binary symmetric channel as a finite stochastic channel. lean/CapacityAtlas/Channels/Binary.lean CapacityAtlas.Channel.binarySymmetric_zero At p=0 the BSC is the identity channel. lean/CapacityAtlas/Channels/Binary.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

Channels with memory Updated 2026-08-09

Binary deletion channel

Open Lean: not started

Each input bit is independently deleted without an erasure marker. The exact capacity is unknown for every nontrivial deletion probability.

\(0.1221(1-d)<C_{\mathrm{del}}(d)\le 0.3578(1-d)\)
2 bounds Open entry
Multi-user Updated 2026-08-09

General discrete memoryless relay channel

Open Lean: not started

A relay assists communication from a source to a destination. Decode-forward and the cut-set bound do not coincide in general.

\(R_{\mathrm{DF}}\le C\le R_{\mathrm{cut}}\)
2 bounds Open entry
Point-to-point Updated 2026-08-09

Real additive white Gaussian noise channel

Solved Lean: not started

The power-constrained real Gaussian channel has a closed-form capacity attained by a Gaussian input.

\(C_{\mathrm{AWGN}}(P,N)=\frac12\log_2\!\left(1+\frac{P}{N}\right)\)
2 bounds Open entry