LemmaStatement: Literature-sourcedProof: AI-generatedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

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-IID rate-distortion mutual-information converse

Statement

Let $S_{1}, \dots, S_{k}$ be IID with law $P_{S}$ on a finite nonempty alphabet $S$ , let $\hat{S}$ be finite nonempty, and let $d : S \times \hat{S} \to [0, \infty)$ be finite-valued. For any joint law of $S^{k}$ and ${\hat{S}}^{k}$ , put $D_{k} : = E d_{k} (S^{k}, {\hat{S}}^{k})$ , using the normalized block distortion of Single-letter and block distortion. If $R (D)$ is the finite-alphabet information rate-distortion function in bits from Finite-alphabet information rate-distortion function, then

$\ln 2 R (D_{k}) \leq \frac{1}{k} I (S^{k}; {\hat{S}}^{k}),$

where mutual information on the right is in nats. The test channel induced by the joint law is feasible at distortion $D_{k}$ , so the rate-distortion minimum is attained there by Attainment of finite-alphabet rate-distortion minima.

Facts & Assumptions

Given: A finite IID source, finite reproduction alphabet, finite nonnegative distortion, and any joint distribution of $S^{k}, {\hat{S}}^{k}$ .

[A1]

$S_{1}, \dots, S_{k}$ are IID with common law $P_{S}$ ; hence each coordinate has law $P_{S}$ and is independent of its predecessors.

[F1]

Finite-alphabet information rate-distortion function and Attainment of finite-alphabet rate-distortion minima: $R (D)$ is the minimum finite mutual information in bits over test channels with source law $P_{S}$ and expected distortion at most $D$ ; every feasible minimum is attained.

[F2]

Single-letter and block distortion: $d_{k} (s^{k}, {\hat{s}}^{k}) = k^{- 1} \sum_{i = 1}^{k} d (s_{i}, {\hat{s}}_{i})$ .

[F3]

Finite mutual information and Finite entropy and mutual-information chain rules: finite mutual information has the chain rule, including $I (U; V, Z) = I (U; Z) + I (U; V ∣ Z)$ .

[F4]

Finite conditional mutual information identities and equality: finite conditional mutual information is nonnegative.

[F5]

Finite information quantities convert by the logarithm base: information in bits equals information in nats divided by $\ln 2$ .

Proof

1.1A1F1F2givenconstruct

Let $T$ be uniform on $[k]$ , independent of $(S^{k}, {\hat{S}}^{k})$ , and put $(S, \hat{S}) = (S_{T}, {\hat{S}}_{T})$ . By [A1], $S$ has law $P_{S}$ ; by [F2], $E d (S, \hat{S}) = k^{- 1} \sum_{i} E d (S_{i}, {\hat{S}}_{i}) = D_{k}$ . For each $s$ with $P_{S} (s) > 0$ , the conditional law of $\hat{S}$ given $S = s$ is a probability vector; choose any probability-vector row for zero-mass $s$ . This gives a finite test channel with source law $P_{S}$ and distortion $D_{k}$ , so it is feasible in [F1].

1.2A1F3F4givenalgebra

The chain rule [F3] gives $I (S^{k}; {\hat{S}}^{k}) = \sum_{i = 1}^{k} I (S_{i}; {\hat{S}}^{k} ∣ S^{i - 1})$ . Since $I (S_{i}; S^{i - 1}) = 0$ by [A1], the chain rule gives $I (S_{i}; {\hat{S}}^{k} ∣ S^{i - 1}) = I (S_{i}; {\hat{S}}^{k}, S^{i - 1})$ . Write $U_{i} = ({\hat{S}}^{k}, S^{i - 1})$ ; its coordinate ${\hat{S}}_{i}$ is a function of $U_{i}$ , so $I (S_{i}; U_{i}, {\hat{S}}_{i}) = I (S_{i}; U_{i})$ . Expanding the left side by [F3] and using [F4] yields $I (S_{i}; U_{i}) = I (S_{i}; {\hat{S}}_{i}) + I (S_{i}; U_{i} ∣ {\hat{S}}_{i}) \geq I (S_{i}; {\hat{S}}_{i})$ . Summing proves $\sum_{i} I (S_{i}; {\hat{S}}_{i}) \leq I (S^{k}; {\hat{S}}^{k})$ .

2.1F1F3F4F5step 1.1step 1.2algebra∎

By the chain rule, $I (S; \hat{S} ∣ T) = k^{- 1} \sum_{i} I (S_{i}; {\hat{S}}_{i})$ . Since $S$ and $T$ are independent, $I (S; \hat{S}, T) = I (S; \hat{S} ∣ T)$ ; also $I (S; \hat{S}, T) = I (S; \hat{S}) + I (S; T ∣ \hat{S}) \geq I (S; \hat{S})$ by [F3]–[F4]. Thus $I (S; \hat{S}) \leq k^{- 1} \sum_{i} I (S_{i}; {\hat{S}}_{i}) \leq k^{- 1} I (S^{k}; {\hat{S}}^{k})$ by step 1.2. The test channel in step 1.1 is feasible, so [F1] gives $R (D_{k}) \leq I_{2} (S; \hat{S})$ , where the subscript denotes bits. Multiply by $\ln 2$ and use [F5] to obtain the claimed nats inequality.

Depends on

Used by

Lossy separation for finite IID sources and finite DMCs Theorem

Dependency tree · two levels

18 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, MIT OpenCourseWare 6.441 Information Theory, Chapter 20: Advanced Channel Coding and Source-Channel Separation (standard reference, not scraped)
Robert M. Gray, Entropy and Information Theory, author-hosted full text (standard reference, not scraped)