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

A Gaussian maximizes scalar differential entropy at fixed variance

Statement

Assume AC. Let $V$ have a Lebesgue density $p$ with $\int p (x) ∣ \ln p (x) ∣ d x < \infty$ , finite mean $μ$ , and positive finite variance $v = E [(V - μ)^{2}]$ . Define $h (V) : = - \int p (x) \ln p (x) d x$ . Then $h (V) \leq \frac{1}{2} \ln (2 π e v),$ with equality exactly when $V \sim N (μ, v)$ .

Facts & Assumptions

Given: AC and a real random variable with a density whose entropy integrand is absolutely integrable, finite mean, and positive finite variance.

[A1]

The Axiom of Choice: AC is required by the stated measure-theoretic KL convention and the Gaussian-law definitions.

[F1]

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

[F2]

Kullback–Leibler divergence is nonnegative: for probability measures, $D (P ∥ Q) \geq 0$ , with equality exactly when $P = Q$ .

[F3]

Standard normal and normal laws and A positive-definite multivariate normal law has its Gaussian density: for $v > 0$ , $N (μ, v)$ has density $(2 π v)^{- 1 / 2} \exp (- (x - μ)^{2} / (2 v))$ .

[F4]

Moments, variance, and covariance on a probability space: $E [(V - μ)^{2}] = v$ .

[F5]

The natural logarithm as the inverse of the exponential function: $\ln$ denotes the natural logarithm.

Proof

1.1A1F1F3F4F5given

Let $q$ be the positive density in [F3]. Since $q (x) > 0$ for every $x$ , the law with density $p$ is absolutely continuous with respect to the Gaussian law. Its KL divergence is well-defined by [F1]. The absolute entropy-integrability hypothesis and finite second moment make each term in the following expansion integrable.

2.1A1F1F2F3F4F5step 1.1algebra∎

Expanding $\ln (p / q)$ and integrating gives $D (P_{V} ∥ N (μ, v)) = - h (V) + \frac{1}{2} \ln (2 π v) + \frac{E [(V - μ)^{2}]}{2 v} = - h (V) + \frac{1}{2} \ln (2 π e v)$ . By [F2] this is nonnegative, proving the bound; equality holds exactly when the two laws coincide, again by [F2].

Depends on

Used by

Finite-input vector Gaussian mutual information is bounded by water-filling Lemma

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

Yury Polyanskiy and Yihong Wu, Information Theory: From Coding to Learning, Chapter 2 §2.3, Theorem 2.8 (standard reference, not scraped)
David J. C. MacKay, Information Theory, Inference, and Learning Algorithms, Chapter 12 §12.3 (standard reference, not scraped)