LemmaStatement: Literature-sourcedProof: AI-generatedPipeline-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.

Gaussian reference-kernel mutual-information lower bound

Statement

Assume AC. Let $X \sim N (0, σ^{2})$ with $σ^{2} > 0$ , let $Y$ be any real-valued reconstruction jointly distributed with $X$ , and suppose $0 < D < σ^{2}$ and $δ : = E (X - Y)^{2} \leq D$ . Then

$I_{n a t} (X; Y) \geq \frac{1}{2} \ln \frac{σ^{2}}{D} .$

No density for $Y$ , conditional differential entropy, or subtraction of potentially infinite entropies is assumed.

Facts & Assumptions

Given: AC, $X \sim N (0, σ^{2})$ , $Y \in R$ , $0 < D < σ^{2}$ , and $δ = E (X - Y)^{2} \leq D$ .

[A1]

The Axiom of Choice: AC is required by the KL and normal-law suppliers below.

[F1]

Mutual information for standard-Borel random elements: $I_{n a t} (X; Y) = D (P_{X Y} ∥ P_{X} \otimes P_{Y})$ .

[F2]

Standard normal and normal laws: $N (m, s)$ , for $s > 0$ , is the affine image of the standard normal with density $(2 π)^{- 1 / 2} e^{- z^{2} / 2}$ .

[F3]

A C^1 diffeomorphism satisfies the change-of-variables formula for nonnegative Lebesgue measurable functions: under Countable Choice, a positive affine change of variable transforms a density by its Jacobian. The assumed AC in [A1] implies Countable Choice by restricting its choice function to a countable family.

[F4]

Kullback–Leibler divergence: for $P ≪ Q$ , $D (P ∥ Q) = \int \ln (d P / d Q) d P$ ; if absolute continuity fails, the divergence is $+ \infty$ .

[F5]

KL chain rule for standard-Borel disintegrations: when two joint laws have the same standard-Borel marginal, their joint KL is the integral of the conditional KL divergences.

[F6]

Kullback–Leibler divergence is nonnegative: under AC, KL divergence between probability laws is nonnegative.

[F7]

Disintegration of a joint law on standard borel spaces: under AC, a joint law of standard-Borel random elements admits a regular conditional kernel for X given Y.

[F8]

Measurability of integration against a kernel and A prior and model kernel define a joint law: a jointly measurable integrand has measurable kernel integrals, and a probability base with a probability kernel defines a joint law with the iterated-integral formula.

[F9]

For sigma-finite factors, the product measure exists, has the rectangle formula, is sigma-finite, and is unique and Tonelli's theorem for nonnegative measurable functions on a sigma-finite product: the product $P_{Y} \otimes λ$ exists and nonnegative product integrals equal their iterated integrals; a strictly positive density gives an equivalent measure by A nonnegative measurable function has integral $0$ exactly when it vanishes almost everywhere.

[F10]

KL is invariant under a measurable bijection: a measurable coordinate swap preserves KL, so $I_{n a t} (X; Y) = D (P_{Y X} ∥ P_{Y} \otimes P_{X})$ .

[F11]

The real line with its Borel sigma-algebra is standard Borel: the real line with its Borel sigma-algebra is standard Borel.

Proof

Given: The hypotheses and suppliers [A1], [F1]–[F6].

1.1A1F1F2F3F8F9F10givenconstruct

By [F2]–[F3], $X \sim N (0, σ^{2})$ has the everywhere-positive density $p_{X} (x) = (2 π σ^{2})^{- 1 / 2} e^{- x^{2} / (2 σ^{2})}$ , and $N (y, D)$ has density $q_{y} (x) = (2 π D)^{- 1 / 2} e^{- (x - y)^{2} / (2 D)}$ . Let $γ = N (0, 1)$ and set $L (y, A) = \int 1_{A} (y + \sqrt{D} z) γ (d z)$ for Borel $A$ . The integrand is product-measurable, so [F8] makes $y \mapsto L (y, A)$ measurable; each $L (y, \cdot) = N (y, D)$ is a probability. Thus [F8] gives a joint law $Q$ on the coordinate order $(Y, X)$ with base $P_{Y}$ and conditional kernel $L$ . By [F9], $Q$ and $P_{Y} \otimes P_{X}$ have respective densities $q_{y} (x)$ and $p_{X} (x)$ relative to $P_{Y} \otimes λ$ , so they are equivalent. If $P_{Y X} ≪̸ P_{Y} \otimes P_{X}$ , [F1] and [F10] give $I_{n a t} (X; Y) = + \infty$ , so the result holds. Otherwise equivalence gives $P_{Y X} ≪ Q$ as well.

2.1A1F1F4F10step 1.1algebra

On the remaining case, the logarithm of the reference-density ratio is $\ln \frac{q_{Y} (X)}{p_{X} (X)} = \frac{1}{2} \ln \frac{σ^{2}}{D} - \frac{(X - Y)^{2}}{2 D} + \frac{X^{2}}{2 σ^{2}} .$ It is integrable because $E (X - Y)^{2} = δ < \infty$ and $E X^{2} = σ^{2}$ . The Radon–Nikodym chain identity $d P_{Y X} / d (P_{Y} \otimes P_{X}) = (d P_{Y X} / d Q) (d Q / d (P_{Y} \otimes P_{X}))$ , integrated using [F4] and [F10], gives $I_{n a t} (X; Y) = D (P_{Y X} ∥ Q) + \frac{1}{2} \ln \frac{σ^{2}}{D} + \frac{1}{2} - \frac{δ}{2 D} .$ The finite cross term prevents an $\infty - \infty$ ambiguity if the first divergence is infinite.

3.1A1F5F6F7F11step 2.1algebra∎

By [F11] the real source and reconstruction spaces are standard Borel, so [F7] supplies a conditional kernel for $X$ given $Y$ under $P_{Y X}$ . The law $Q$ has the same $Y$ -marginal and conditional kernel $N (y, D)$ . Thus [F5] expresses $D (P_{Y X} ∥ Q)$ as an integral of conditional KL divergences, which is nonnegative by [F6], including the value $+ \infty$ . Also $δ \leq D$ , so $1 / 2 - δ / (2 D) \geq 0$ . The identity in step 2.1 gives the claimed lower bound.

Depends on

Used by

Dependency tree · two levels

103 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

Robert M. Gray, Source Coding Theory, first edition (standard reference, not scraped)
MIT OpenCourseWare 6.441, Chapter 25: Evaluating R(D) (standard reference, not scraped)