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

Bounded densities with finite second moments have finite differential entropy

Statement

Let $f$ be a Lebesgue probability density on $R^{d}$ with $∥ f ∥_{\infty} < \infty$ and $\int ∣ x ∣^{2} f (x) d x < \infty$ . Then $\int f (x) ∣ \ln f (x) ∣ d x < \infty$ , so the differential entropy in Differential entropy for real densities is a finite real number.

Facts & Assumptions

Given: A Lebesgue probability density $f$ with finite essential supremum and finite second moment.

[F1]

Differential entropy for real densities: differential entropy is defined by $h (f) = - \int f \ln f$ in the absolutely integrable case.

Proof

1.1givenalgebra

Let $q (x) = (2 π)^{- d / 2} e^{- ∣ x ∣^{2} / 2}$ and $M = \max {1, ∥ f ∥_{\infty}}$ . On ${f > 1}$ , $f \ln f \leq f \ln M$ , so the positive part is integrable. For $t \geq 0$ , $t \ln (1 / t) \leq 1 / e$ ; with $t = f / q$ , this gives $f \ln (q / f) \leq q / e$ . Thus on ${f \leq 1}$ , $- f \ln f = f \ln (q / f) - f \ln q \leq q / e + f ∣ \ln q ∣ .$ The right side is integrable because $q$ is a probability density and $∣ \ln q ∣$ is bounded by a constant plus $∣ x ∣^{2} / 2$ . Hence the negative part of $f \ln f$ is integrable.

2.1F1step 1.1algebra∎

Both parts of $f \ln f$ are integrable by step 1.1. Therefore $\int f ∣ \ln f ∣ < \infty$ , and [F1] defines a finite differential entropy.

Depends on

Differential entropy for real densities

Used by

Dependency tree · one level

1 result within one dependency step 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)