Channel and question
- Input
- \(X\in\{0,1\}\)
- Output
- \(Y\in\{0,1\}\)
- Law
- \(Y=X\oplus Z\), where \(Z\sim\mathrm{Bernoulli}(p)\) independently across uses.
- Quantity
- Shannon capacity \(C_{\mathrm{BSC}}(p)\), measured in bits per channel use.
Criterion. Average-error capacity.
- The range p at most 1/2 removes the equivalent relabelled regime.
- Average decoding error vanishes with blocklength.
Parameters
- \(p\)
- Crossover probability. Range: \(0\le p\le1/2\).
Current status
\[C_{\mathrm{BSC}}(p)=1-h_2(p)\]
Conditions. \(0\le p\le1/2\).
The uniform input distribution achieves capacity.
| Result | Relation | Method | Year |
|---|---|---|---|
| Lower | \(C\ge1-h_2(p)\) | Apply the DMC coding theorem to independent uniform inputs. | 1948 |
| Upper | \(C\le1-h_2(p)\) | Maximize mutual information; symmetry makes the uniform input optimal. | 1948 |
Formal verification
Lean coverageFormally stated
The single-letter information capacity is proved from reusable finite-distribution and entropy APIs. The operational average-error formula is proved locally by applying the formal finite-channel coding theorem.
Claims
- For 0 ≤ p ≤ 1/2, the single-letter information capacity is 1-h₂(p) bits per use.
information-capacity· exact capacity · solved · Formally proved · v2 - For 0 ≤ p ≤ 1/2, operational vanishing-average-error capacity is 1-h₂(p) bits per use.
operational-capacity· exact capacity · solved · Formally proved · v2
Lean declarations (6)
CapacityAtlas.FiniteChannel.informationCapacityBits_eq_binarySymmetricAPI
lean/CapacityAtlasForMathlib/InformationTheory/BinarySymmetric.lean — Information capacity of any finite channel with binary-symmetric transition rows.CapacityAtlas.FiniteChannel.operationalCapacityBitsAPI
lean/CapacityAtlasForMathlib/InformationTheory/OperationalCapacity.lean — Operational average-error capacity defined through block codes and vanishing error.CapacityAtlas.Channel.binarySymmetricdefinition
lean/CapacityAtlas/Channels/Binary.lean — Binary symmetric channel as a finite stochastic channel.CapacityAtlas.Channel.binarySymmetric_zerotest
lean/CapacityAtlas/Channels/Binary.lean — At p=0 the channel is the identity.CapacityAtlas.Channel.binarySymmetric_informationCapacityclaim · information-capacity
lean/CapacityAtlas/Channels/Binary.lean — For 0 ≤ p ≤ 1/2, the single-letter information capacity is 1-h₂(p) bits per use.CapacityAtlas.Channel.binarySymmetric_operationalCapacityclaim · operational-capacity
lean/CapacityAtlas/Channels/Binary.lean — For 0 ≤ p ≤ 1/2, operational vanishing-average-error capacity is 1-h₂(p) 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.
- Thomas M. Cover and Joy A. Thomas (2006). Elements of Information Theory. Wiley, second edition. DOI 10.1002/047174882X.