Capacity Atlas Channel-capacity problems
Point-to-point

Real additive white Gaussian noise channel

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

Solved Lean: not started AWGN
01 · Model

Channel specification

Input

\(X \in \mathbb{R}\)

Output

\(Y \in \mathbb{R}\)

Law

Y=X+Z, where Z\sim\mathcal{N}(0,N) is independent across channel uses.

Parameters

SymbolMeaningRange
\(P\) Average input power constraint. \(P \ge 0\)
\(N\) Noise variance per channel use. \(N > 0\)

Assumptions

  • The encoder satisfies \mathbb{E}[X^2]\le P.
  • Average probability of error vanishes with blocklength.
02 · Capacity

Shannon capacity

bits per channel use exact
\[C_{\mathrm{AWGN}}(P,N)=\frac12\log_2\!\left(1+\frac{P}{N}\right)\]

Conditions. P\ge 0 and N>0.

A zero-mean Gaussian input with variance P achieves capacity.

Symbol
\(C_{\mathrm{AWGN}}(P,N)\)
Error criterion
Average-error capacity without feedback.
03 · Evidence

Known bounds and characterizations

TypeClaimMethodSource
lower \(C\ge \frac12\log_2(1+P/N)\) Gaussian random coding and typical decoding. 1948 [1]
upper \(C\le \frac12\log_2(1+P/N)\) The Gaussian distribution maximizes differential entropy at fixed variance. 1948 [1]
04 · History

Bound timeline

  1. 1948

    Shannon identified the Gaussian-channel capacity formula and coding theorem.

    Reference
05 · Lean

Formalization status

Lean: not started

Not started

The initial Lean library covers finite channels. Continuous probability and differential entropy are a later milestone.

  1. Definitions
  2. Statement
  3. Partial proof
  4. Complete proof

No Lean file is linked yet. A contribution should begin by reusing the shared definitions under lean/CapacityAtlas.

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.

\(C_{\mathrm{BSC}}(p)=1-h_2(p)\)
2 bounds Open entry
Point-to-point Updated 2026-08-09

Binary erasure channel

Solved Lean: definitions

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

\(C_{\mathrm{BEC}}(\varepsilon)=1-\varepsilon\)
2 bounds Open entry
Point-to-point Updated 2026-08-09

Binary Z-channel

Solved Lean: definitions

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

\(C_Z(p)=\log_2\!\left(1+(1-p)p^{p/(1-p)}\right)\)
2 bounds Open entry