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.

Second-order exponential upper bound on the nonpositive axis

Statement

For every real $z \leq 0$ ,

\exp (z) \leq 1 + z + \frac{z^{2}}{2} .

Facts & Assumptions

Given: A real number $z \leq 0$ and the real exponential function.

[F1]

The real exponential function and the number $e$ by a power series: $\exp (0) = 1$ .

[F2]

The exponential function is smooth and $(\exp)^{'} = \exp$ : the real exponential is $C^{\infty}$ , with derivative $(\exp)^{'} = \exp$ .

[F3]

The exponential function is strictly increasing: $\exp$ is strictly increasing on $R$ .

[F4]

Mean value theorem on a closed real interval: a function continuous on $[a, b]$ and differentiable on $(a, b)$ has $f (b) - f (a) = f^{'} (c) (b - a)$ for some $c \in (a, b)$ .

Proof

1.1givenF1F2F3F4construct

If $z = 0$ , the claim is equality. For $z < 0$ , fix any $a < b \leq 0$ and set $g (t) = 1 + t - \exp (t)$ . By [F2], $g^{'} (t) = 1 - \exp (t) \geq 0$ for $t \leq 0$ , because [F3] and [F1] give $\exp (t) \leq \exp (0) = 1$ . Applying [F4] to $g$ on $[a, b]$ shows $g (b) - g (a) = g^{'} (c) (b - a) \geq 0$ , so $g$ is nondecreasing on $(- \infty, 0]$ .

2.1givenF1F2F4step 1.1algebra∎

For the remaining case $z < 0$ , step 1.1 shows $g (t) \leq 0$ for every $t \leq 0$ . Set $f (t) = 1 + t + t^{2} / 2 - \exp (t)$ ; then $f^{'} (t) = g (t)$ . Applying [F4] on $[z, 0]$ gives $f (0) - f (z) = g (c) (- z) \leq 0$ . Since $f (0) = 0$ , $f (z) \geq 0$ , which is the required inequality.

Depends on

Used by

Dependency tree · two levels

19 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

Tor Lattimore and Csaba Szepesvári, Bandit Algorithms (standard reference, not scraped)