LemmaStatement: Literature-sourcedProof: AI-generatedPipeline-generated

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

The capacity-achieving output law is unique

Statement

For a finite DMC $W$ , every input law attaining $C (W) = \max_{P} I (P, W)$ induces the same output law $Q^{*}$ . This output law is unique even when the capacity-achieving input law is not.

Facts & Assumptions

Given: A finite DMC $W$ and $C (W) = \max_{P} I (P, W)$ .

[F1]

Finite DMC information capacity is attained: at least one input law attains $C (W)$ .

[F2]

Single-letter information capacity of a finite DMC: $C (W)$ is the maximum of $I (P, W)$ over input probability vectors.

[F3]

Finite mutual information and Finite distributions, entropy, divergence, and stochastic matrices: finite mutual information is the finite joint/product KL sum and $H (q) = - \sum_{y : q_{y} > 0} q_{y} \ln q_{y}$ .

[F4]

Finite discrete memoryless channels: every row $W (\cdot ∣ x)$ is a probability vector and $P W$ is the induced output law.

[F5]

The natural logarithm has derivative 1/x and equals the integral from 1 to x of 1/t and Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ : logarithmic differentiation and the product rule apply on positive coordinates.

[F6]

The logarithm grows more slowly than every positive real power: $t \ln t \to 0$ as $t ↓ 0$ .

Proof

1.1F3F4givenalgebra

Expanding the finite KL sum in [F3] for the joint law $P (x) W (y ∣ x)$ and grouping its finite terms gives $I (P, W) = H (P W) - \sum_{x} P (x) H (W (\cdot ∣ x)) .$ Terms with zero probability are omitted, so this identity also holds on the boundary of the input simplex.

1.2F3F4F5F6given

Suppose capacity-achieving laws $P_{0}, P_{1}$ have distinct outputs $Q_{0}, Q_{1}$ . Their midpoint input $\overset{ˉ}{P} = (P_{0} + P_{1}) / 2$ has output $\overset{ˉ}{Q} = (Q_{0} + Q_{1}) / 2$ . The scalar function $- t \ln t$ is strictly concave for $t > 0$ because its second derivative, computed using [F3] and the product rule, is $- 1 / t$ ; continuity at $0$ from [F6] and the direct identity $- \frac{t}{2} \ln \frac{t}{2} > - \frac{t}{2} \ln t$ when one endpoint is zero extend strict concavity to the closed interval. Hence finite entropy is strictly concave and $H (\overset{ˉ}{Q}) > (H (Q_{0}) + H (Q_{1})) / 2$ .

2.1F1F2step 1.1step 1.2assume-contradischarge-contradiction∎

The second term in step 1.1 is linear in $P$ , so step 1.2 gives $I (\overset{ˉ}{P}, W) > (I (P_{0}, W) + I (P_{1}, W)) / 2 = C (W)$ , contradicting [F2]. Existence in [F1] and this contradiction show that all capacity-achieving input laws induce one common output law.

Depends on

Used by

Dependency tree · two levels

38 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Yury Polyanskiy and Yihong Wu, Information Theory: From Coding to Learning, Chapters 19 and 22 (standard reference, not scraped)