Channel and question
- Input
- \(X\in\{1,\ldots,q\}\)
- Output
- \(Y=X\)
- Law
- \(W(y|x)=\mathbf 1\{y=x\}\).
- Quantity
- Shannon capacity \(C\), measured in bits per channel use.
Criterion. Zero-error and average-error capacities coincide.
- Channel uses are independent.
- Rates are measured in bits.
Parameters
- \(q\)
- Alphabet size. Range: \(q\ge2\).
Current status
\[C=\log_2 q\]
| Result | Relation | Method | Year |
|---|---|---|---|
| Lower | \(C\ge\log_2 q\) | Transmit one q-ary symbol per use. | 1948 |
| Upper | \(C\le\log_2 q\) | There are only q outputs per use. | 1948 |
Formal verification
Lean coverageFormally stated
The information-capacity formula is proved by reducing mutual information to input entropy. The operational average-error formula follows from the formal finite-channel coding theorem.
Claims
- For q ≥ 2, the single-letter information capacity is log₂ q bits per use.
information-capacity· exact capacity · solved · Formally proved · v1 - For q ≥ 2, operational vanishing-average-error capacity is log₂ q bits per use.
operational-capacity· exact capacity · solved · Formally proved · v1
Lean declarations (4)
CapacityAtlas.FiniteChannel.identityAPI
lean/CapacityAtlasForMathlib/InformationTheory/FiniteChannel.lean — Noiseless finite channel.CapacityAtlas.FiniteChannel.operationalCapacityBitsAPI
lean/CapacityAtlasForMathlib/InformationTheory/OperationalCapacity.lean — Operational average-error capacity defined through block codes and vanishing error.CapacityAtlas.Channel.noiseless_informationCapacityclaim · information-capacity
lean/CapacityAtlas/Channels/Noiseless.lean — For q ≥ 2, the single-letter information capacity is log₂ q bits per use.CapacityAtlas.Channel.noiseless_operationalCapacityclaim · operational-capacity
lean/CapacityAtlas/Channels/Noiseless.lean — For q ≥ 2, operational vanishing-average-error capacity is log₂ q bits per use.
References
- Claude E. Shannon (1948). A Mathematical Theory of Communication. Bell System Technical Journal. DOI 10.1002/j.1538-7305.1948.tb01338.x.