ExampleConstruction: AI-adaptedVerification: 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.

Entropy-divergence example

Example

Let $w_{n} : = {\begin{cases} 0, & n \in {0, 1}, \\ \frac{1}{C n (\log n)^{2}}, & n \geq 2, \end{cases} C : = \sum_{n \geq 2} \frac{1}{n (\log n)^{2}},$ where $\log$ is the natural logarithm. This example verifies concretely that:

(a) the normalizing constant is finite and positive, $C \in (0, \infty)$ , so that $\sum_{n \geq 0} w_{n} = 1$ (Series and absolute convergence in a normed space);

(b) the entropy of the weight family diverges, $s (w) : = - \sum_{n \geq 0} w_{n} \log w_{n} = \sum_{n \geq 0} w_{n} \log \frac{1}{w_{n}} = + \infty,$ where the sum is the nonnegative extended sum of the nonnegative terms $w_{n} \log (1 / w_{n})$ ; for a zero weight, both expressions $- w_{n} \log w_{n}$ and $w_{n} \log (1 / w_{n})$ are defined to have value $0$ . Thus the two zero weights at $n = 0, 1$ contribute $0$ rather than requiring a logarithm or reciprocal at zero;

(c) Consequently, a probability weight on a countable set can have infinite entropy, while every finite probability vector $p = (p_{1}, \dots, p_{d})$ with $p_{i} \geq 0$ and $\sum_{i} p_{i} = 1$ has entropy $s_{d} (p) : = - \sum_{i : p_{i} > 0} p_{i} \log p_{i} \leq \log d$ (zero entries contribute $0$ ). The finite bound is verified below.

Verification

Given: the weight family $(w_{n})_{n \in N}$ and the constant $C$ defined above.

[F1] Cauchy condensation: for a nonnegative nonincreasing family $(a_{k})_{k \geq 1}$ , $\sum_{k \geq 1} a_{k}$ converges if and only if $\sum_{j \geq 0} 2^{j} a_{2^{j}}$ converges (For a nonincreasing nonnegative sequence, $\sum a_{k}$ converges iff $\sum 2^{k} a_{2^{k}}$ converges).

[F2] $p$ -series: $\sum_{k \geq 1} k^{- p}$ converges if and only if $p > 1$ ; in particular $\sum_{k \geq 1} k^{- 2} < \infty$ and $\sum_{k \geq 1} k^{- 1} = \infty$ (The p-series for a real exponent p converges exactly when p is greater than one).

[F3] For $x \geq 1$ , $\log x = \int_{1}^{x} d t / t$ with $0 \leq \log x \leq x - 1$ and $1 - 1 / x \leq \log x$ (The natural logarithm as the inverse of the exponential function, The natural logarithm has derivative 1/x and equals the integral from 1 to x of 1/t, 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)$ ).

[F4] The natural logarithm is continuous, strictly increasing and onto $R$ , satisfies $\log 1 = 0$ , the product and reciprocal laws, and is inverse to the real exponential (Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm, The natural logarithm as the inverse of the exponential function).

1.1F1F2F3algebra

[Finiteness of $C$ ] The family $a_{k} : = 1 / (k (\log k)^{2})$ , $k \geq 2$ , is nonnegative and nonincreasing for $k \geq 3$ (the denominator $k (\log k)^{2}$ is increasing by [F3] applied to $\log$ ), so condensation [F1] applied to the tail from $k \geq 2$ reduces $\sum_{k \geq 2} a_{k}$ to $\sum_{j \geq 1} 2^{j} a_{2^{j}} = \sum_{j \geq 1} \frac{2^{j}}{2^{j} (\log 2^{j})^{2}} = \frac{1}{(\log 2)^{2}} \sum_{j \geq 1} \frac{1}{j^{2}}$ , which converges by [F2]; the finitely many terms with $k = 2$ do not affect convergence. Since every term is positive, $C \in (0, \infty)$ and therefore $\sum_{n} w_{n} = C / C = 1$ .

1.2F1F2algebra

[Divergence of the comparison series] Again by [F1], $\sum_{k \geq 3} \frac{1}{k \log k}$ converges if and only if $\sum_{j \geq 2} \frac{2^{j}}{2^{j} \log (2^{j})} = \frac{1}{\log 2} \sum_{j \geq 2} \frac{1}{j}$ converges, which fails by [F2] with $p = 1$ ; hence $\sum_{k \geq 3} 1 / (k \log k) = + \infty$ .

1.3F3F4algebra

[The entropy lower bound] Put $R : = \max (0, - \frac{1}{2} \log C)$ . Since $\log$ is onto, choose $x_{0} > 0$ with $\log x_{0} = e^{R}$ ; for every integer $n \geq \max {2, x_{0}}$ , monotonicity gives $\log n \geq e^{R}$ and then $\log \log n \geq R$ . Thus $\log C + 2 \log \log n \geq 0$ . By the product and reciprocal laws [F4], $\log \frac{1}{w_{n}} = \log C + \log n + 2 \log \log n \geq \log n > 0$ for all such $n$ , and $w_{n} \log \frac{1}{w_{n}} \geq \frac{1}{C n (\log n)^{2}} \log n = \frac{1}{C n \log n}$ .

2.1step 1.1step 1.2step 1.3algebra

[Divergence of the entropy] Since all terms $w_{n} \log (1 / w_{n})$ are nonnegative, the extended sum $s (w) = \sum_{n \geq 0} w_{n} \log (1 / w_{n})$ dominates any finite partial sum; by step 1.3 it dominates $\frac{1}{C} \sum_{N \leq n \leq M} \frac{1}{n \log n}$ for all large $N \leq M$ , and step 1.2 shows that these partial sums are unbounded as $M \to \infty$ . Hence $s (w) = + \infty$ , proving (b) and, with step 1.1, the countable-set claims (a)-(b).

3.1F3F4step 1.1step 2.1algebra∎

[The finite-dimensional entropy bound] Let $S : = {i : p_{i} > 0}$ and $k : = ∣ S ∣$ , so $1 \leq k \leq d$ . For every $x \geq 1$ , [F3] gives $\log x \leq x - 1$ ; for $0 < x < 1$ , put $y = 1 / x > 1$ and use [F3] with [F4] to get $\log x = - \log y \leq - (1 - 1 / y) = x - 1$ . Therefore, using the logarithm laws [F4] and $\sum_{i \in S} p_{i} = 1$ , $s_{d} (p) - \log d = \sum_{i \in S} p_{i} \log \frac{1}{d p_{i}} \leq \sum_{i \in S} p_{i} (\frac{1}{d p_{i}} - 1) = \frac{k}{d} - 1 \leq 0.$ This proves the finite-dimensional bound in (c); together with steps 1.1-2.1 it establishes (a)-(c).

Entropy-divergence example

Example

Verification

Depends on

Dependency tree · 2 levels

Sources