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

Negative entropy on the simplex is strongly convex and has range log n

Statement

Let $n \geq 2$ . Coordinates in $R^{n - 1}$ use the library's function-space convention: for $v \in R^{n - 1}$ and $1 \leq i < n$ , write $v_{i} : = v (i - 1)$ . Let

$K_{n} : = {q \in R^{n - 1} : q_{i} \geq 0 for all 1 \leq i < n, \sum_{i = 1}^{n - 1} q_{i} \leq 1},$

and for $q \in K_{n}$ put $p_{i} = q_{i}$ for $1 \leq i < n$ and $p_{n} = 1 - \sum_{i = 1}^{n - 1} q_{i}$ . Define $R (q) = \sum_{i = 1}^{n} p_{i} \log p_{i}$ , with $0 \log 0 : = 0$ . In the independent coordinates $q_{1}, \dots, q_{n - 1}$ , $R$ is continuous on $K_{n}$ , is twice continuously differentiable on its interior, is $1$ -strongly convex in the Euclidean norm, and satisfies

$- \log n \leq R (q) \leq 0.$

The minimum $- \log n$ is attained at $p_{i} = 1 / n$ for every $i$ , and the maximum $0$ is attained at each vertex of the simplex.

Statement references

Mirror maps, Bregman divergence, and local Hessian norms: defines strong convexity by the displayed Euclidean quadratic inequality and defines the interior Hessian norms used by this regularizer.

A convex subset of $R^{m}$ contains every line segment between two of its points: convexity means every segment between simplex points remains in the simplex.

Facts & Assumptions

Given: An integer $n \geq 2$ and the finite simplex $K_{n}$ with the coordinates and boundary convention in the Statement.

[F1]

Mirror maps, Bregman divergence, and local Hessian norms: a regularizer is strongly convex with constant $m$ when $R ((1 - λ) x + λ y) \leq (1 - λ) R (x) + λ R (y) - \frac{m}{2} λ (1 - λ) ∥ x - y ∥_{2}^{2}$ ; its Hessian is the matrix of second partial derivatives.

[F2]

The natural logarithm has derivative 1/x and equals the integral from 1 to x of 1/t: $(\log x)^{'} = 1 / x$ for $x > 0$ .

[F3]

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$ supplies the product rule, and The chain rule, in one line from Carathéodory: if $g$ is differentiable at $c$ and $f$ is differentiable at $g (c)$ , then $f \circ g$ is differentiable at $c$ with $(f \circ g)^{'} (c) = f^{'} (g (c)) g^{'} (c)$ supplies the chain rule for differentiable scalar compositions. These apply to $s \log s$ and to its affine coordinate substitutions on the simplex interior.

[F4]

Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm: $\log$ is continuous and strictly increasing, $\log 1 = 0$ , and $\log (1 / x) = - \log x$ for $x > 0$ .

[F5]

The natural logarithm is bounded above by its positive argument minus one: $0 \leq \log u \leq u - 1$ for $u \geq 1$ .

[F6]

A twice-differentiable function on an open interval is convex if and only if its second derivative is nonnegative: on an open real interval, a twice-differentiable scalar function is convex if its second derivative is nonnegative everywhere.

[F7]

Finite Jensen inequality for convex functions on $R^{n}$ : for a convex scalar function and finitely many points in its convex domain, its value at a convex combination is at most the same combination of its values.

[F8]

A convex subset of $R^{m}$ contains every line segment between two of its points: a set is convex when it contains every segment between its points; $K_{n}$ is convex because its nonnegativity and sum-at-most-one inequalities are preserved by convex combinations.

Proof

1.1givenF3F4F5algebra

For $0 < x \leq 1$ , set $u = x^{- 1 / 2} \geq 1$ . Then $∣ x \log x ∣ = 2 x \log u \leq 2 x (u - 1) \leq 2 \sqrt{x}$ by [F4, F5], and $2 \sqrt{x} \to 0$ as $x ↓ 0$ . Thus $s \mapsto s \log s$ , defined to be $0$ at $s = 0$ , is continuous on $[0, 1]$ , and its finite sum $R$ is continuous on $K_{n}$ .

1.2givenF2F3algebra

On the interior, differentiation using [F2, F3] gives $\partial_{i} R = \log q_{i} - \log p_{n}$ and $\nabla^{2} R (q) = diag (1 / q_{1}, \dots, 1 / q_{n - 1}) + \frac{1}{p_{n}} 11^{⊤}$ . Since $0 < q_{i} \leq 1$ and $p_{n} > 0$ , $v^{⊤} (\nabla^{2} R (q) - I) v = \sum_{i < n} (1 / q_{i} - 1) v_{i}^{2} + (\sum_{i < n} v_{i})^{2} / p_{n} \geq 0$ .

2.1givenstep 1.2F1F6F8algebra

For interior $q, r$ , [F8] keeps $(1 - s) q + s r$ in $K_{n}$ . The restriction $s \mapsto R ((1 - s) q + s r) - \frac{1}{2} ∥ (1 - s) q + s r ∥_{2}^{2}$ has nonnegative second derivative on $0 < s < 1$ by step 1.2, hence is convex there by [F6]; continuity extends its convexity inequality to $s = 0, 1$ . Expanding the squared norm yields the strong-convexity inequality with constant $1$ from the definition in [F1] for interior $q, r$ .

2.2givenF2F3F6step 1.1algebra

Each $p_{i} \in [0, 1]$ gives $p_{i} \log p_{i} \leq 0$ , so $R (q) \leq 0$ . The scalar function $ϕ (s) = s \log s$ , extended by $ϕ (0) = 0$ , is continuous by step 1.1 and convex on $(0, 1)$ because $ϕ^{''} (s) = 1 / s > 0$ ; [F6] and continuity extend convexity to $[0, 1]$ .

3.1givenF1step 1.1step 2.1algebra

Let $e$ be the uniform point of $K_{n}$ . For arbitrary $q, r \in K_{n}$ and $0 < ϵ < 1$ , both $(1 - ϵ) q + ϵ e$ and $(1 - ϵ) r + ϵ e$ are interior. Apply step 2.1 to them and let $ϵ ↓ 0$ ; step 1.1 gives continuity, so the same inequality in [F1] holds for all $q, r \in K_{n}$ .

4.1givenF4F7F8step 2.2algebra∎

Apply [F7] to $p_{1}, \dots, p_{n}$ with equal weights $1 / n$ . Since their average is $1 / n$ , it gives $R (q) / n \geq ϕ (1 / n) = - (\log n) / n$ , so $R (q) \geq - \log n$ . At the uniform point equality holds, while at a vertex the only nonzero summand is $1 \log 1 = 0$ ; these attain both endpoints.

Depends on

Used by

Negative entropy gives normalized multiplicative weights Example

Dependency tree · two levels

46 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

Elad Hazan, Introduction to Online Convex Optimization, second edition (standard reference, not scraped)
Peter Bartlett, Stat 260/CS 294-102: Learning in Sequential Decision Problems, mirror-descent lecture notes (standard reference, not scraped)