LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck pending

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.

Power bound for real and complex scalar Gaussian channels

Statement

Assume AC. Let $X$ be real or complex with finite second moment, let $Z$ be independent unit-variance Gaussian noise, and let $Y = a X + Z$ . In the real case take $Z \sim N (0, 1)$ and $a \in R$ ; in the complex case take $Z \sim C N (0, 1)$ with density $π^{- 1} e^{- ∣ z ∣^{2}}$ and $a \in C$ . Put $v = E ∣ X - E X ∣^{2}$ and $κ = 1 / 2$ in the real case, $κ = 1$ in the complex case. Then $I (X; Y) \leq κ \ln (1 + ∣ a ∣^{2} v) \leq κ \ln (1 + ∣ a ∣^{2} E ∣ X ∣^{2})$ in nats; division by $\ln 2$ gives the corresponding bit formula. Equality in the first inequality holds when $X$ is Gaussian in the real case or circular complex Gaussian in the complex case, including the zero-variance case.

Facts & Assumptions

Given: AC, an input law with finite second moment, independent unit-variance Gaussian noise of the stated type, and the scalar channel $Y = a X + Z$ .

[A1]

The Axiom of Choice: AC is inherited from the real and complex Gaussian entropy bounds and the measure-theoretic information definition.

[F1]

Measure-theoretic mutual information: $I (X; Y)$ is the KL divergence from the joint law to the product of its marginals.

[F2]

Differential entropy for real densities: when $Y$ has a density with absolutely integrable $f_{Y} \ln f_{Y}$ , $h (Y) = - \int f_{Y} \ln f_{Y}$ .

[F3]

Gaussian maximizes differential entropy at fixed positive-definite covariance: for real $Y$ , $h (Y) \leq \frac{1}{2} \ln (2 π e Var Y)$ .

[F4]

Circular complex Gaussian maximizes differential entropy at fixed second moment: for complex $Y$ , $h (Y) \leq \ln (π e E ∣ Y - E Y ∣^{2})$ .

[F5]

Bounded densities with finite second moments have finite differential entropy: a bounded density with finite second moment has absolutely integrable $f \ln f$ .

Proof

1.1F2F5givenalgebra

The output density is the convolution $f_{Y} (y) = \int g_{Z} (y - a x) P_{X} (d x)$ , so $0 < f_{Y} \leq ∥ g_{Z} ∥_{\infty} < \infty$ , and $Y$ has finite second moment. By [F5], $\int f_{Y} ∣ \ln f_{Y} ∣ < \infty$ , so [F2] defines a finite differential entropy $h (Y)$ .

2.1A1F1F2step 1.1algebra

The positive Gaussian noise density makes $f_{Y} (y) > 0$ . Relative to $P_{X} (d x) f_{Y} (y) d y$ , the joint law of $(X, Y)$ has density $g_{Z} (y - a x) / f_{Y} (y)$ . By [F1], $I (X; Y) = \int P_{X} (d x) \int g_{Z} (y - a x) \ln \frac{g_{Z} (y - a x)}{f_{Y} (y)} d y = h (Y) - h (Z) .$ The two logarithmic integrals are finite by step 1.1 and the Gaussian density formula, so this identity involves no subtraction of infinite quantities.

3.1F3F4step 2.1givenalgebra∎

Independence gives $Var (Y) = 1 + ∣ a ∣^{2} v$ . Apply [F3] and the real Gaussian noise entropy in the real case, or [F4] and $h (Z) = \ln (π e)$ in the complex case. Step 2.1 then yields $I (X; Y) \leq κ \ln (1 + ∣ a ∣^{2} v)$ nats. Since $v \leq E ∣ X ∣^{2}$ , division by $\ln 2$ gives the corresponding bit bound. For the stated Gaussian inputs, the output is Gaussian of the same real or circular complex type and attains the matching maximum-entropy equality.

Depends on

Used by

Dependency tree · two levels

15 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, author prepublication (standard reference, not scraped)
John Duchi, Lecture Notes on Statistics and Information Theory (standard reference, not scraped)