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.

Finite-simplex entropy is continuous and concave

Statement

For a finite nonempty alphabet of size $m$ , let $H (p) : = - \sum_{i = 1}^{m} p_{i} \ln p_{i}, 0 \ln 0 : = 0,$ on the probability simplex $Δ_{m} = {p \in [0, 1]^{m} : \sum_{i} p_{i} = 1}$ . Then $H$ is continuous and concave on $Δ_{m}$ , with $0 \leq H (p) \leq \ln m$ .

Facts & Assumptions

Given: An integer $m \geq 1$ and the finite probability simplex $Δ_{m}$ .

[F1]

The natural logarithm as the inverse of the exponential function: $\ln$ is the natural logarithm on $(0, \infty)$ .

[F2]

The logarithm grows more slowly than every positive real power: $\ln s / s \to 0$ as $s \to + \infty$ .

[F3]

The natural logarithm has derivative 1/x and equals the integral from 1 to x of 1/t and Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ : for $t > 0$ , $(\ln t)^{'} = 1 / t$ , so the second derivative of $- t \ln t$ is $- 1 / t$ .

[F4]

A twice-differentiable function on an open interval is convex if and only if its second derivative is nonnegative: a twice-differentiable function with nonpositive second derivative on an interval is concave there, by applying the nonnegative-second-derivative criterion to its negative.

Proof

1.1F1F2givenalgebra

Define $h (t) = - t \ln t$ for $0 < t \leq 1$ and $h (0) = 0$ . With $s = 1 / t$ , $∣ t \ln t ∣ = \ln (s) / s \to 0$ as $t ↓ 0$ by [F1] and [F2]; hence $h$ is continuous on $[0, 1]$ .

2.1F3F4step 1.1algebra

On $(0, 1)$ , [F3] gives $h^{''} (t) = - 1 / t < 0$ , so [F4] makes $h$ concave there. For $u, v \in [0, 1]$ and $0 < ϵ < 1$ , replace each endpoint by $u_{ϵ} = (1 - ϵ) u + ϵ / 2$ and $v_{ϵ} = (1 - ϵ) v + ϵ / 2$ . Concavity on $(0, 1)$ applies to these interior points; taking $ϵ ↓ 0$ and using step 1.1 gives the concavity inequality on the closed interval.

3.1step 1.1step 2.1givenalgebra

For $p, q \in Δ_{m}$ and $0 \leq θ \leq 1$ , apply the concavity inequality for $h$ to each coordinate $θ p_{i} + (1 - θ) q_{i}$ . Summing the $m$ inequalities gives $H (θ p + (1 - θ) q) \geq θ H (p) + (1 - θ) H (q)$ . Continuity of $H$ follows from continuity of the finite sum of the coordinate functions $h$ .

4.1F1step 3.1givenalgebracases∎

Each summand $- p_{i} \ln p_{i}$ is nonnegative because $0 \leq p_{i} \leq 1$ , so $H (p) \geq 0$ . The average of the $m!$ coordinate permutations of $p$ is the uniform vector $u = (1 / m, \dots, 1 / m)$ , and each permutation has entropy $H (p)$ . Concavity from step 3.1, iterated over this finite average, gives $H (u) \geq H (p)$ . Since $H (u) = \ln m$ , the claimed upper bound follows, including $m = 1$ .

Depends on

Used by

Dependency tree · two levels

28 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 1 §1.1 and Chapter 2 §2.3 (standard reference, not scraped)
David J. C. MacKay, Information Theory, Inference, and Learning Algorithms, Chapter 12 §12.3 (standard reference, not scraped)