LemmaStatement: Literature-sourcedProof: AI-generatedPipeline-generatedprecheck pass

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 finite Rényi generators are convex with stated boundary values

Statement

For $α > 1$ , the generator $h_{α} (t) = t^{α} - 1$ is convex on $(0, \infty)$ , satisfies $h_{α} (1) = 0$ , has $h_{α} (0 +) = - 1$ , and has recession limit $\lim_{t \to \infty} h_{α} (t) / t = + \infty$ . For $0 < α < 1$ , the generator $g_{α} (t) = 1 - t^{α}$ is convex on $(0, \infty)$ , satisfies $g_{α} (1) = 0$ , has $g_{α} (0 +) = 1$ , and has recession limit $\lim_{t \to \infty} g_{α} (t) / t = 0$ .

Facts & Assumptions

Given: The positive-base power functions in the Statement and the corresponding exponent range.

[F1]

Real powers for positive bases, with the zero-base positive-exponent convention: for $t > 0$ , $t^{γ} = \exp (γ \log t)$ .

[F2]

Continuity and derivatives of positive-base real powers 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$ : $(t^{γ})^{'} = γ t^{γ - 1}$ and the derivative algebra rules hold for real $γ$ .

[F3]

A twice-differentiable function on an open interval is convex if and only if its second derivative is nonnegative and Convex and strictly convex functions on Euclidean convex sets: a twice differentiable function on an open interval is convex when its second derivative is nonnegative there.

[F4]

The natural logarithm as the inverse of the exponential function and Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm: $\log$ is an increasing surjection onto $R$ and $\log (1 / t) = - \log t$ .

[F5]

The exponential tends to $+ \infty$ at $+ \infty$ and to $0$ at $- \infty$ : $\exp u \to + \infty$ as $u \to + \infty$ , and $\exp u > 0$ .

[F6]

The exponential is positive and satisfies $\exp (- x) = 1 / \exp (x)$ : $\exp (- u) = 1 / \exp (u)$ for every real $u$ .

Proof

1.1F1F4F5givenalgebra

Let $γ > 0$ . As $t \to + \infty$ , $\log t \to + \infty$ because [F4] is increasing and onto. Hence $γ \log t \to + \infty$ , so $t^{γ} = \exp (γ \log t) \to + \infty$ by [F1, F5].

1.2F1F4F5F6givenalgebra

Let $γ > 0$ and put $s = 1 / t$ . As $t ↓ 0$ , $s \to + \infty$ . By [F1], [F4], and [F6], $t^{γ} = \exp (- γ \log s) = 1 / \exp (γ \log s) \to 0$ by [F5].

2.1F1F2F3step 1.1step 1.2algebra

For $α > 1$ , [F2] gives $h_{α}^{''} (t) = α (α - 1) t^{α - 2} > 0$ , so [F3] proves convexity; also $h_{α} (1) = 0$ . By step 1.2, $h_{α} (0 +) = 0^{α} - 1 = - 1$ . By step 1.1 with $γ = α - 1$ , $t^{α - 1} \to + \infty$ , and $1 / t \leq 1$ for $t \geq 1$ , so $h_{α} (t) / t = t^{α - 1} - 1 / t \to + \infty$ .

3.1F1F2F3step 1.2constructalgebra∎

For $0 < α < 1$ , [F2] gives $g_{α}^{''} (t) = α (1 - α) t^{α - 2} > 0$ , so [F3] proves convexity; also $g_{α} (1) = 0$ . By step 1.2, $g_{α} (0 +) = 1$ . Put $u = 1 / t$ . As $t \to + \infty$ , $u ↓ 0$ , and step 1.2 with $γ = 1 - α$ gives $u^{1 - α} \to 0$ , that is, $t^{- (1 - α)} \to 0$ . For $t \geq 1$ , $0 \leq ∣ g_{α} (t) / t ∣ = t^{- (1 - α)} - 1 / t \leq t^{- (1 - α)}$ . Therefore $g_{α} (t) / t \to 0$ .

Depends on

Used by

Finite data processing for Rényi divergence Theorem

Dependency tree · two levels

36 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 7, §§7.1 and 7.12 (standard reference, not scraped)
Tim van Erven and Peter Harremoës, Rényi Divergence and Kullback-Leibler Divergence, §II-A (standard reference, not scraped)