Channel and question
- Input
- \(X\in\{0,1\}\)
- Output
- \(Y\in\{0,1\}\)
- Law
- \(P(Y=0\mid X=0)=1\) and \(P(Y=0\mid X=1)=p\).
- Quantity
- Shannon capacity \(C_Z(p)\), measured in bits per channel use.
Criterion. Average-error capacity.
- Channel uses are independent.
- Average decoding error vanishes with blocklength.
Parameters
- \(p\)
- Probability that input 1 is received as 0. Range: \(0\le p\le1\).
Current status
\[C_Z(p)=\log_2\!\left(1+(1-p)p^{p/(1-p)}\right)\]
Conditions. \(0<p<1\), with endpoints by continuity.
The optimizing input is generally nonuniform.
| Result | Relation | Method | Year |
|---|---|---|---|
| Lower | \(C_Z(p)\ge\log_2\!\left(1+(1-p)p^{p/(1-p)}\right)\) | Evaluate mutual information at the optimizing Bernoulli input. | 1948 |
| Upper | \(C_Z(p)\le\log_2\!\left(1+(1-p)p^{p/(1-p)}\right)\) | Apply the DMC converse and solve the one-variable maximization. | 1948 |
Formal verification
Lean coverageFormally stated
The proof uses a binary entropy log-partition inequality and the finite-DMC coding theorem. Both endpoints are proved directly. Lean’s totalized powers and division give the endpoint values.
Claims
- The closed-form single-letter information capacity, including one bit at p=0 and zero at p=1.
information-capacity· exact capacity · solved · Formally proved · v1 - The closed-form operational vanishing-average-error capacity for every 0 ≤ p ≤ 1.
operational-capacity· exact capacity · solved · Formally proved · v1 - An explicit Bernoulli input attains capacity, with probability of input 1 equal to p^(p/(1-p))/(1+(1-p)p^(p/(1-p))) in the interior.
optimizing-input· structural · solved · Formally proved · v1
Lean declarations (7)
CapacityAtlas.Channel.binaryZdefinition
lean/CapacityAtlas/Channels/Binary.lean — Binary Z-channel as a finite stochastic channel.CapacityAtlas.Channel.binaryZOptimalInputdefinition
lean/CapacityAtlas/Channels/BinaryZ.lean — Explicit capacity-achieving Bernoulli distribution, including both endpoints.CapacityAtlas.Channel.binaryZ_informationCapacityclaim · information-capacity
lean/CapacityAtlas/Channels/BinaryZ.lean — The exact information-capacity formula on the full closed parameter interval.CapacityAtlas.Channel.binaryZ_operationalCapacityclaim · operational-capacity
lean/CapacityAtlas/Channels/BinaryZ.lean — The exact operational average-error capacity from the finite-DMC coding theorem.CapacityAtlas.Channel.binaryZ_optimalInputclaim · optimizing-input
lean/CapacityAtlas/Channels/BinaryZ.lean — The explicit Bernoulli input attains the operational capacity.CapacityAtlas.Channel.binaryZ_zerotest
lean/CapacityAtlas/Channels/BinaryZ.lean — The noiseless endpoint has capacity one and the explicit input is uniform.CapacityAtlas.Channel.binaryZ_onetest
lean/CapacityAtlas/Channels/BinaryZ.lean — The constant-output endpoint has capacity zero, attained by every input.
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.