TheoremStatement: 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.

Reliable average-error DMC rates do not exceed capacity

Statement

For any sequence of fixed-length codes over a finite DMC with average errors $ε_{a v} (n) \to 0$ , one has ${lim sup}_{n \to \infty} n^{- 1} \ln M_{n} \leq C (W)$ .

Facts & Assumptions

Given: A finite DMC $W$ and a length- $n$ code with $M$ messages, uniform message $J$ , input word $X^{n} = e (J)$ , output $Y^{n}$ , and estimate $\hat{J} = d (Y^{n})$ .

[F1]

Finite-alphabet Fano inequality: for a uniform variable on $M$ messages decoded from $Y^{n}$ with error probability $ε$ , $H (J ∣ Y^{n}) \leq \ln 2 + ε \ln M$ .

[F2]

Finite entropy and mutual-information chain rules: $I (J; Y^{n}) = H (J) - H (J ∣ Y^{n}) = H (Y^{n}) - H (Y^{n} ∣ J)$ , with all terms finite.

[F3]

Fixed-length codes for a finite DMC and Finite discrete memoryless channels: $X^{n}$ is a deterministic function of $J$ , and conditional on $J = m$ the output law is $W^{n} (\cdot ∣ e (m))$ .

[F4]

The n-letter mutual information of a DMC is at most nC: $I (X^{n}; Y^{n}) \leq n C (W)$ for every input law.

Proof

1.1F2F3givenalgebra

Since the encoder is deterministic and the channel law given $J = m$ depends on $m$ only through $X^{n} = e (m)$ , $H (Y^{n} ∣ J) = H (Y^{n} ∣ X^{n})$ . By [F2], $I (J; Y^{n}) = I (X^{n}; Y^{n})$ .

2.1F1F2F4step 1.1algebra

By [F1] and [F2], $\ln M = I (J; Y^{n}) + H (J ∣ Y^{n}) \leq I (X^{n}; Y^{n}) + \ln 2 + ε_{a v} \ln M \leq n C (W) + \ln 2 + ε_{a v} \ln M$ using [F4].

3.1step 2.1givenalgebra∎

For a reliable code sequence, rearrange step 2.1 to get $(1 - ε_{a v} (n)) n^{- 1} \ln M_{n} \leq C (W) + n^{- 1} \ln 2$ . The left coefficient tends to one and the right side tends to $C (W)$ , so $lim sup n^{- 1} \ln M_{n} \leq C (W)$ .

Depends on

Used by

Operational capacity formula for a finite DMC Theorem

Dependency tree · two levels

23 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 17 §17.3 and Chapter 19 §19.1 (standard reference, not scraped)
Robert Gallager, Principles of Digital Communication I, Chapter 8 §8.7.3, MIT OpenCourseWare (standard reference, not scraped)