CCapacity Atlas
finite-dmc-input-cost

Finite discrete memoryless channel with input cost

A finite DMC under a feasible maximum-codeword average-cost constraint has a constrained mutual-information capacity formula.

Point-to-point Finite alphabet Discrete memoryless Capacity Exact Single-letter characterization

Channel and question

Input
Symbols in a finite alphabet \(\mathcal X\), with cost \(c(x)\ge0\).
Output
Symbols in a finite alphabet \(\mathcal Y\).
Law
A stationary memoryless transition law \(W(y\mid x)\).
Quantity
Cost-constrained capacity \(C(\Gamma)\), measured in bits per channel use.

Criterion. Arbitrary blocklength deterministic codes with maximum-codeword cost and vanishing average error.

  • Every codeword has average input cost at most \(\Gamma\).
  • At least one input symbol has cost at most \(\Gamma\).
  • Messages are uniform and average decoding error vanishes.

Current status

\[C(\Gamma)=\max_{P_X:\,\mathbb E[c(X)]\le\Gamma} I(X;Y)\]
Known results and bounds for Finite discrete memoryless channel with input cost
ResultRelationMethodYear
Exact\(C(\Gamma)=\max_{P_X:\,\mathbb E[c(X)]\le\Gamma}I(X;Y)\)Cost-constrained channel coding theorem and convex optimization.2015

Formal verification

Lean coverageFormally stated

The local proof uses cost-controlled random coding and a finite-mixture converse. It covers the minimum feasible budget and proves that an admissible input attains the information supremum.

Claims

  • For nonnegative cost with a feasible symbol, maximum-codeword-cost operational capacity equals constrained information capacity.
    exact-capacity · exact capacity · solved · Formally proved · v1
Lean declarations (1)
  • CapacityAtlas.FiniteChannel.finiteDMCInputCostCapacityStatement claim · exact-capacity
    lean/CapacityAtlas/Channels/InputCost.lean — For nonnegative cost with a feasible symbol, maximum-codeword-cost operational capacity equals constrained information capacity.
Linked proofs (1)
  • exact-capacity · complete · claim v1
    TomasOrtega/CapacityAtlasInputCost@5e6a432b · CapacityAtlasCost.finiteDMCInputCostCapacity
    Historical upstream certificate imported into this repository; the original immutable proof link is retained as provenance.

References

  1. Tobias Sutter, David Sutter, Peyman Mohajerin Esfahani, and John Lygeros (2015). Efficient Approximation of Channel Capacities. IEEE Transactions on Information Theory. DOI 10.1109/TIT.2015.2401002.
  2. Victoria Kostina and Sergio Verdú (2015). Channels with Cost Constraints: Strong Converse and Dispersion. IEEE Transactions on Information Theory.

Discussion

Find discussionStart discussion

Related problems

Binary Z-channel Z-channel

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

Point-to-point Binary Finite alphabet Discrete memoryless Asymmetric Capacity Exact
Solved \(C_Z(p)=\log_2\!\left(1+(1-p)p^{p/(1-p)}\right)\)
Binary erasure channel BEC

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

Point-to-point Binary Finite alphabet Discrete memoryless Symmetric Erasure Capacity Exact
Solved \(C_{\mathrm{BEC}}(\varepsilon)=1-\varepsilon\)
Binary memory with encoder-known stuck-at defects

Independent stuck-at defects are known noncausally to the encoder but not the decoder.

Point-to-point Binary Finite alphabet Discrete memoryless Noncausal state information Capacity Exact
Solved \(C=1-\delta\)
Binary symmetric channel BSC

Each bit is independently flipped with probability \(p\).

Point-to-point Binary Finite alphabet Discrete memoryless Symmetric Capacity Exact
Solved \(C_{\mathrm{BSC}}(p)=1-h_2(p)\)