ExampleConstruction: Literature-sourcedVerification: 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.

The uniform law has infinite self-information entropy and zero differential entropy

Statement

Assume AC (and hence countable choice). Let $P$ be Lebesgue measure restricted to the Borel unit interval $[0, 1]$ , and let $X$ be the identity random element on that probability space. Its law entropy $H (X) = I (X; X)$ is $+ \infty$ , whereas its differential entropy is $0$ .

Facts & Assumptions

Given: AC (and hence countable choice) and $P (A) = λ_{1} (A)$ for Borel $A \subseteq [0, 1]$ .

[A1]

AC is used by the self-information KL definition; it implies the countable choice required by the box-volume formula. The Axiom of Choice The Axiom of Countable Choice ( ${A C}_{ω}$ )

[F1]

Borel sets are Lebesgue measurable; Lebesgue measure is a measure, and every one-dimensional box with finite endpoints, including a degenerate closed interval, has measure its length under countable choice. Lebesgue measurable sets, the family $L (R^{n})$ , and the restricted set function $λ_{n}$ Assuming countable choice, $L (R^{n})$ is a sigma-algebra containing every elementary set and $λ_{n}$ is a complete measure extending elementary volume Assuming countable choice, every Borel subset of $R^{n}$ is Lebesgue measurable A box in $R^{n}$ with parameters $a_{i} \leq b_{i}$ is Lebesgue measurable of measure $\prod_{i < n} (b_{i} - a_{i})$ , whichever of its faces are included

[F2]

The Borel unit interval is standard Borel. The unit interval with its Borel structure is standard Borel

[F3]

For a standard-Borel law, self-information entropy is infinite whenever its atomic set has probability less than one. Law entropy as self-mutual information Self-mutual-information entropy on countable and non-atomic laws

[F4]

Differential entropy for a Lebesgue density $f$ is $- \int f \ln f d λ_{1}$ , with $0 \ln 0 = 0$ ; the nonnegative Lebesgue integral of the zero function is zero. Law entropy and differential entropy are different quantities The nonnegative Lebesgue integral

Proof

Given: The hypotheses in the Statement.

1.1A1F1given

Define $P (A) = λ_{1} (A)$ for Borel $A \subseteq [0, 1]$ . By [F1], these sets are Lebesgue measurable and the restricted measure is countably additive; the box formula gives $P ([0, 1]) = 1$ , so P is a probability. For each $x \in [0, 1]$ , the degenerate interval $[x, x] = {x}$ has measure $x - x = 0$ . Thus every singleton has P-mass zero, and the atomic set $S = {x : P ({x}) > 0}$ is empty.

2.1F2F3step 1.1

The identity map on $[0, 1]$ has law P, and its value space is standard Borel by [F2]. Since $P (S) = 0 < 1$ , [F3] gives $H (X) = + \infty$ .

3.1F1F4algebra∎

Extending the density by zero outside $[0, 1]$ gives $f = 1_{[0, 1]}$ . On the interval $f \ln f = 1 \ln 1 = 0$ , and off the interval the integrand is zero by the convention in [F4]. Thus $f \ln f$ is the zero function on $R$ ; its integral is zero by [F4], so the differential entropy is $h (f) = 0$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

67 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, Entropy and Information Theory, corrected author-hosted first edition, Chapters 1 and 5 §5.5 (standard reference, not scraped)
John Duchi, Lecture Notes on Statistics and Information Theory, Chapter 2 §2.1 (standard reference, not scraped)