ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-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.

No side information reduces Wyner-Ziv to ordinary rate distortion

Example

Let $Y$ be a constant random variable, let $X$ have any finite law, and let $d : X \times \hat{X} \to [0, d_{\max}]$ be finite. Define the ordinary finite single-letter information rate in nats by $R_{X, d}^{n a t} (D) : = \inf_{P_{\hat{X} ∣ X} : E d (X, \hat{X}) \leq D} I (X; \hat{X})$ . Then decoder-only side information is absent and $R_{W Z} (D) = R_{X, d}^{n a t} (D)$ .

Facts & Assumptions

Given: A finite source law $P_{X}$ , a constant $Y$ , finite reproduction alphabet, finite bounded distortion, and feasible $D$ .

[F1]

Finite-alphabet memoryless Wyner-Ziv theorem: $R_{W Z} (D)$ minimizes $I (X; U ∣ Y)$ over finite $U - X - Y$ and $\hat{X} = g (Y, U)$ subject to the expected distortion constraint.

[F2]

Finite mutual information: $I (X; \hat{X})$ is the finite joint-law KL in nats, so the displayed ordinary single-letter infimum uses the same units as $R_{W Z}$ .

[F3]

Finite-alphabet lossy source coding with decoder-only side information: a finite auxiliary $U$ and decoder map $g (Y, U)$ define a stochastic reproduction channel from $X$ ; when $Y$ is constant and $U = \hat{X}$ , the decoder returns that reproduction letter.

[F4]

Data processing for a finite Markov chain, with equality condition: for a finite Markov chain $X \to U \to \hat{X}$ , $I (X; \hat{X}) \leq I (X; U)$ .

Verification

1.1F1F2F4algebra

Because $Y$ is constant, any Wyner-Ziv test channel and reconstruction induce a finite channel $P_{\hat{X} ∣ X}$ with $\hat{X} = g (U)$ . Its distortion is unchanged and $X - U - \hat{X}$ is a Markov chain. By [F2] and [F4], $R_{X, d}^{n a t} (D) \leq I (X; \hat{X}) \leq I (X; U ∣ Y) = I (X; U)$ . Taking the infimum over WZ test channels gives $R_{X, d}^{n a t} (D) \leq R_{W Z} (D)$ .

2.1F1F2F3step 1.1algebra∎

Conversely, every finite channel $P_{\hat{X} ∣ X}$ feasible for the ordinary infimum in [F2] gives the WZ test channel $U = \hat{X}$ and decoder $g (y, u) = u$ . This is feasible with the same mutual information and distortion, by [F3]. Taking infima gives $R_{W Z} (D) \leq R_{X, d}^{n a t} (D)$ . Together with step 1.1 this proves equality.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

24 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

Thomas M. Cover and Joy A. Thomas, Elements of Information Theory, second edition (standard reference, not scraped)
Aaron D. Wyner and Jacob Ziv, The Rate-Distortion Function for Source Coding with Side Information at the Decoder (standard reference, not scraped)