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.

IID DMC information density converges to mutual information

Statement

Fix a finite DMC $W$ and input law $P_{X}$ . If $(X_{i}, Y_{i})_{i \geq 1}$ are IID with law $P_{X} (x) W (y ∣ x)$ , then $n^{- 1} ı_{P_{X}} (X^{n}; Y^{n}) \to I (P_{X}; W)$ in probability.

Facts & Assumptions

Given: A finite DMC $W$ , an input probability vector $P_{X}$ , and IID pairs with joint law $P_{X} (x) W (y ∣ x)$ .

[F1]

Finite DMC information density: on positive joint support, $ı_{P_{X}} (x; y) = \ln (W (y ∣ x) / Q_{P_{X}} (y))$ .

[F2]

Finite mutual information: $I (P_{X}; W)$ is the finite sum of the joint mass times the log ratio of joint mass to product-marginal mass.

[F3]

Finite stochastic kernels: each row $W (\cdot ∣ x)$ is a probability vector.

Proof

1.1F1F2F3givenalgebra

On every pair with $P_{X} (x) W (y ∣ x) > 0$ , the output marginal $Q_{P_{X}} (y)$ is positive. Thus [F1] gives a finite value, and summing its expectation gives $E [ı_{P_{X}} (X_{1}; Y_{1})] = \sum_{x, y : P_{X} (x) W (y ∣ x) > 0} P_{X} (x) W (y ∣ x) \ln \frac{W (y ∣ x)}{Q_{P_{X}} (y)} = I (P_{X}; W)$ by [F2]. The variable has finite support, hence some finite variance $v$ . The row-law normalization is supplied by [F3].

2.1F1step 1.1givenalgebra∎

Let $S_{n} : = \sum_{i = 1}^{n} ı_{P_{X}} (X_{i}; Y_{i})$ . Independence gives $E S_{n} = n I (P_{X}; W)$ and $E [(S_{n} - E S_{n})^{2}] = n v$ . For every $η > 0$ , the squared deviation is at least $n^{2} η^{2}$ on ${∣ S_{n} / n - I (P_{X}; W) ∣ \geq η}$ , so that event has probability at most $v / (n η^{2}) \to 0$ . This is convergence in probability.

Depends on

Used by

Dependency tree · two levels

14 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.2 (standard reference, not scraped)
Robert Gallager, Principles of Digital Communication I, Chapter 8 §8.7.4, MIT OpenCourseWare (standard reference, not scraped)