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

Finite KL nonnegativity for subprobability references

Statement

Proves $\ln t \leq t - 1$ for $t > 0$ and, for finite probability weights $p$ and positive-on-support reference weights $q$ with $\sum_{i} q_{i} \leq 1$ , proves $\sum_{i : p_{i} > 0} p_{i} \log_{2} (p_{i} / q_{i}) \geq 0$ by an explicit finite argument without choice.

Facts & Assumptions

Given: A finite probability vector $p = (p_{i})$ and nonnegative reference weights $q_{i}$ with $q_{i} > 0$ whenever $p_{i} > 0$ and $\sum_{i} q_{i} \leq 1$ .

[F1]

Finite-block information and entropy in bits: $\log_{2} t = \ln t / \ln 2$ and $\ln 2 > 0$ .

[F2]

The integral logarithm $L (x) : = \int_{1}^{x} \frac{d t}{t}$ for $x > 0$ : $L (t) = \int_{1}^{t} d u / u$ , with oriented limits.

[F3]

The integral logarithm $L$ is the published natural logarithm: $L (t) = \log t$ for $t > 0$ .

[F4]

If $f \leq g$ on $[a, b]$ and both are integrable then $\int_{a}^{b} f \leq \int_{a}^{b} g$ ; and $m (b - a) \leq \int_{a}^{b} f \leq M (b - a)$ : if integrable functions obey a pointwise order on an interval with increasing endpoints, their integrals obey the same order.

[F5]

The natural logarithm as the inverse of the exponential function: $\log$ is the natural logarithm, the inverse of $\exp$ .

[F6]

Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm: $\log$ is strictly increasing and $\log 1 = 0$ .

[F7]

The integral with oriented limits: $\int_{a}^{a} f : = 0$ and $\int_{b}^{a} f : = - \int_{a}^{b} f$ : reversing the integration endpoints changes the sign.

Proof

Given: The finite weights and hypotheses above.

1.1F2F3F4F5F6F7algebra

The integral logarithm is the natural logarithm by [F3] and [F5]. If $t > 1$ , then $1 / u \leq 1$ on $[1, t]$ , so [F2]–[F4] give $\ln t = \int_{1}^{t} d u / u \leq t - 1$ . If $0 < t < 1$ , then $1 / u \geq 1$ on $[t, 1]$ , so $\int_{t}^{1} d u / u \geq 1 - t$ ; [F3] and [F7] give $\ln t = - \int_{t}^{1} d u / u \leq t - 1$ . At $t = 1$ , [F6] gives equality. Therefore $\ln t \leq t - 1$ for all $t > 0$ .

2.1F1step 1.1givenalgebra∎

Apply step 1.1 to $t = q_{i} / p_{i}$ for every $i$ with $p_{i} > 0$ . Then $\sum_{i : p_{i} > 0} p_{i} \ln (p_{i} / q_{i}) = - \sum_{i : p_{i} > 0} p_{i} \ln (q_{i} / p_{i}) \geq \sum_{i : p_{i} > 0} (p_{i} - q_{i}) = 1 - \sum_{i : p_{i} > 0} q_{i} \geq 0.$ Dividing by $\ln 2 > 0$ gives the same nonnegativity for the bit-log sum. Thus finite KL nonnegativity against a subprobability reference, as well as the logarithm inequality used to prove it, follows from finite sums and elementary integral bounds; no choice axiom enters.

Depends on

Used by

Dependency tree · two levels

29 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 (standard reference, not scraped)