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.

Finite DMC information capacity is attained

Statement

For every finite DMC $W$ , the supremum $C (W)$ is a maximum: there is an input probability vector $P_{X}^{*}$ such that $I (P_{X}^{*}; W) = C (W)$ .

Facts & Assumptions

Given: A finite DMC $W$ with finite nonempty input alphabet $X$ and output alphabet $Y$ .

[F1]

Single-letter information capacity of a finite DMC: $C (W) = \sup_{P_{X}} I (P_{X}; W)$ over probability vectors on $X$ .

[F2]

Finite mutual information and Finite entropy and mutual-information chain rules: for the induced finite joint law, $I (X; Y) = H (Y) - H (Y ∣ X)$ .

[F3]

Finite conditional entropy and Finite distributions, entropy, divergence, and stochastic matrices: $H (Y ∣ X) = \sum_{x} P_{X} (x) H (W (\cdot ∣ x))$ and $H (q) = - \sum_{y} q_{y} \ln q_{y}$ , with $0 \ln 0 = 0$ .

[F4]

The logarithm grows more slowly than every positive real power: $\ln s / s \to 0$ as $s \to + \infty$ , so $- t \ln t \to 0$ as $t ↓ 0$ .

[F5]

For a nonempty subset of $R^{n}$ with $n \geq 1$ , compactness, closedness and boundedness, pseudocompactness, and attainment of extrema by every continuous real-valued function are equivalent: a continuous real function on a nonempty closed bounded subset of finite-dimensional Euclidean space attains a maximum.

Proof

1.1F1F2F3givenalgebra

For an input law $P_{X}$ , let $Q_{P_{X}} = P_{X} W$ . By [F2] and [F3], $I (P_{X}; W) = H (Q_{P_{X}}) - \sum_{x} P_{X} (x) H (W (\cdot ∣ x))$ . The second term is linear in $P_{X}$ .

2.1F3F4step 1.1algebra

The scalar summand $- t \ln t$ , extended by $0$ at $t = 0$ , is continuous on $[0, 1]$ by [F4]. Each coordinate of $Q_{P_{X}}$ is linear in $P_{X}$ , so the finite sum $H (Q_{P_{X}})$ is continuous on the input simplex. Therefore $P_{X} \mapsto I (P_{X}; W)$ is continuous.

3.1F1step 2.1F5choose∎

The input simplex is nonempty because $X$ is nonempty; it is closed and bounded in $R^{∣ X ∣}$ . By [F5], the continuous mutual-information function attains a maximum at some $P_{X}^{*}$ . Its maximum equals the supremum in [F1], proving $I (P_{X}^{*}; W) = C (W)$ .

Depends on

Used by

Cited to discharge well-definedness by Single-letter information capacity of a finite DMC.

Dependency tree · two levels

30 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, Chapter 19 §§19.1–19.2 (standard reference, not scraped)
Robert Gallager, Principles of Digital Communication I, Chapter 8 §8.7.2, MIT OpenCourseWare (standard reference, not scraped)