Capacity Atlas Channel-capacity problems
Point-to-point

Binary erasure channel

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

Solved Lean: definitions BEC
01 · Model

Channel specification

Input

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

Output

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

Law

Y=X with probability 1-\varepsilon and Y=? with probability \varepsilon.

Parameters

SymbolMeaningRange
\(\varepsilon\) Erasure probability. \(0\le\varepsilon\le1\)

Assumptions

  • Channel uses are independent.
  • Average probability of error vanishes with blocklength.
02 · Capacity

Shannon capacity

bits per channel use exact
\[C_{\mathrm{BEC}}(\varepsilon)=1-\varepsilon\]

Conditions. 0\le\varepsilon\le1.

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

Known bounds and characterizations

TypeClaimMethodSource
lower \(C\ge1-\varepsilon\) Random coding, or linear erasure-correcting codes approaching the unerased fraction. 1948 [1]
upper \(C\le1-\varepsilon\) At most one bit can pass through each unerased output position. 1948 [1]
04 · History

Bound timeline

  1. 1948

    The general discrete-memoryless coding theorem gives the formula by mutual-information maximization.

    Reference
05 · Lean

Formalization status

Lean: definitions

Definitions

The transition kernel and its stochasticity proof are formalized. The operational capacity theorem is not yet formalized.

  1. Definitions
  2. Statement
  3. Partial proof
  4. Complete proof
CapacityAtlas.Channel.binaryErasure Binary erasure channel as a finite stochastic 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
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.

\(C_{\mathrm{BSC}}(p)=1-h_2(p)\)
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