Channel and question
- Input
- \(X\in\{1,\ldots,q\}\)
- Output
- \(Y\in\{1,\ldots,q\}\)
- Law
- \(P(Y=X)=1-p\); conditioned on an error, the \(q-1\) other symbols are equiprobable.
- Quantity
- Shannon capacity \(C_q(p)\), measured in bits per channel use.
Criterion. Average-error capacity.
- Channel uses are independent.
- The parameter range uses the usual monotone-noise convention.
Parameters
- \(q\)
- Alphabet size. Range: \(q\ge2\).
- \(p\)
- Total crossover probability. Range: \(0\le p\le(q-1)/q\).
Current status
\[C_q(p)=\log_2 q-h_2(p)-p\log_2(q-1)\]
The uniform input achieves capacity.
| Result | Relation | Method | Year |
|---|---|---|---|
| Lower | \(C_q(p)\ge\log_2 q-h_2(p)-p\log_2(q-1)\) | Uniform input and the DMC coding theorem. | 1948 |
| Upper | \(C_q(p)\le\log_2 q-h_2(p)-p\log_2(q-1)\) | The converse for weakly symmetric channels. | 1948 |
Formal verification
Lean coverageFormally stated
The channel is constructed as additive noise on ZMod q. Its noise entropy is proved to be binary entropy plus p times log(q-1), and the operational formula follows from the finite-group result and coding theorem.
Claims
- For q ≥ 2 and 0 ≤ p ≤ (q-1)/q, information capacity is log₂q-h₂(p)-p log₂(q-1).
information-capacity· exact capacity · solved · Formally proved · v1 - For q ≥ 2 and 0 ≤ p ≤ (q-1)/q, operational capacity is log₂q-h₂(p)-p log₂(q-1).
operational-capacity· exact capacity · solved · Formally proved · v1
Lean declarations (6)
CapacityAtlas.Channel.qarySymmetricNoisedefinition
lean/CapacityAtlas/Channels/QarySymmetric.lean — Symmetric noise distribution on the cyclic q-symbol alphabet.CapacityAtlas.Channel.qarySymmetricdefinition
lean/CapacityAtlas/Channels/QarySymmetric.lean — q-ary symmetric channel as a finite additive-noise channel.CapacityAtlas.Channel.qarySymmetric_transitiontest
lean/CapacityAtlas/Channels/QarySymmetric.lean — The additive construction has the registered q-ary symmetric transition probabilities.CapacityAtlas.FiniteChannel.operationalCapacityBitsAPI
lean/CapacityAtlasForMathlib/InformationTheory/OperationalCapacity.lean — Operational average-error capacity defined through block codes and vanishing error.CapacityAtlas.Channel.qarySymmetric_informationCapacityclaim · information-capacity
lean/CapacityAtlas/Channels/QarySymmetric.lean — For q ≥ 2 and 0 ≤ p ≤ (q-1)/q, information capacity is log₂q-h₂(p)-p log₂(q-1).CapacityAtlas.Channel.qarySymmetric_operationalCapacityclaim · operational-capacity
lean/CapacityAtlas/Channels/QarySymmetric.lean — For q ≥ 2 and 0 ≤ p ≤ (q-1)/q, operational capacity is log₂q-h₂(p)-p log₂(q-1).
References
- Claude E. Shannon (1948). A Mathematical Theory of Communication. Bell System Technical Journal. DOI 10.1002/j.1538-7305.1948.tb01338.x.
- Thomas M. Cover and Joy A. Thomas (2006). Elements of Information Theory. Wiley, second edition. DOI 10.1002/047174882X.