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

KL divergence between equal-variance Gaussian location laws

Statement

Assume AC and let $a, b \in R$ and $τ > 0$ . For the normal location laws with common variance $τ^{2}$ , $D (N (a, τ^{2}) ∥ N (b, τ^{2})) = \frac{(a - b)^{2}}{2 τ^{2}} .$

Facts & Assumptions

Given: AC, real means $a, b$ , and a positive scale $τ$ .

[A1]

The Axiom of Choice: AC supplies the normal-law construction and the Radon–Nikodym assumptions used by the KL definition.

[F1]

Standard normal and normal laws: $N (a, τ^{2})$ is the law of $a + τ Z$ when $Z$ has standard normal law, whose density is $ϕ (z) = (2 π)^{- 1 / 2} e^{- z^{2} / 2}$ .

[F2]

The standard normal density has total mass one: $ϕ$ is a probability density on $R$ .

[F3]

AC supplies countable selections and prescribed serial paths: AC supplies countable choice, the axiom required by the change-of-variables supplier.

[F4]

A C^1 diffeomorphism satisfies the change-of-variables formula for nonnegative Lebesgue measurable functions: for a $C^{1}$ diffeomorphism $T$ and nonnegative measurable $g$ , $\int g (y) d y = \int g (T (x)) ∣ T^{'} (x) ∣ d x$ .

[F5]

Integrating against a density agrees with integrating the product: $\int g d (f d μ) = \int g f d μ$ for nonnegative measurable $f, g$ .

[F6]

The natural logarithm as the inverse of the exponential function: the natural logarithm is the inverse of the real exponential, so $\log (\exp y) = y$ . For positive $u, v$ , $\log (u / v) = \log u - \log v$ (Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm).

[F7]

Multivariate normal law, including singular covariance: a normal law with mean $a$ has expectation $a$ ; in dimension one this is the scalar law $N (a, τ^{2})$ .

[F8]

Kullback–Leibler divergence: for $P ≪ Q$ , $D (P ∥ Q) = \int \log (d P / d Q) d P$ .

Proof

1.1A1F1F2F3F4F5givenconstruct

Set $p_{a} (x) = \frac{1}{τ \sqrt{2 π}} \exp (- \frac{(x - a)^{2}}{2 τ^{2}})$ . Apply [F4] to $g p_{a}$ with $T (z) = a + τ z$ ; since $τ p_{a} (a + τ z) = ϕ (z)$ by [F1], for every nonnegative Borel $g$ , $\int g (x) p_{a} (x) d x = \int g (a + τ z) ϕ (z) d z .$ Thus $N (a, τ^{2})$ has Lebesgue density $p_{a}$ ; the same calculation gives $p_{b}$ for $N (b, τ^{2})$ . Both are strictly positive. Let $r = p_{a} / p_{b}$ . By [F5], $\int_{E} r d N (b, τ^{2}) = \int_{E} p_{a} d x = N (a, τ^{2}) (E)$ for every Borel set $E$ , so $r = d N (a, τ^{2}) / d N (b, τ^{2})$ .

1.2F1F6F7algebra

For every $x$ , cancel the common positive prefactor of $p_{a}$ and $p_{b}$ and apply the quotient law and inverse identity in [F6] to obtain $\log \frac{p_{a} (x)}{p_{b} (x)} = \frac{(x - b)^{2} - (x - a)^{2}}{2 τ^{2}} = \frac{(a - b) (2 x - a - b)}{2 τ^{2}} .$ This affine function is integrable under $N (a, τ^{2})$ , whose mean is $a$ by [F7].

2.1A1F8step 1.2algebra∎

By [F8] and step 1.2, $D (N (a, τ^{2}) ∥ N (b, τ^{2})) = \int \frac{(a - b) (2 x - a - b)}{2 τ^{2}} N (a, τ^{2}) (d x) = \frac{(a - b) (2 a - a - b)}{2 τ^{2}} = \frac{(a - b)^{2}}{2 τ^{2}} .$ The identity also covers $a = b$ , when both sides are zero.

Depends on

Used by

A dense Gaussian mean lower bound by Assouad’s method Example
A Gaussian two-point lower bound Example
A sparse Gaussian sequence lower bound by Fano’s method Example
Equal-variance Gaussian location KL Example
Gaussian sparse-sequence minimax lower bound Theorem

Dependency tree · two levels

71 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

Philippe Rigollet and Jan-Christian Hütter, High-Dimensional Statistics: Lecture Notes, Chapter 4, Example 4.7 (standard reference, not scraped)
John Duchi, Lecture Notes on Statistics and Information Theory, Chapter 2, Example 2.1.7; Chapter 8, Example 8.4.4 (standard reference, not scraped)