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

Scalar exponential bound for bounded losses

Statement

For $0 < η \leq 1$ and $x \in [- 1, 1]$ , $\exp (- η x) \leq 1 - η x + η^{2} .$ Consequently, if $M = M^{*}$ and $- I ⪯ M ⪯ I$ , then $\exp (- η M) ⪯ I - η M + η^{2} I$ .

Facts & Assumptions

Given: $0 < η \leq 1$ , $x \in [- 1, 1]$ , and a Hermitian matrix $M$ with $- I ⪯ M ⪯ I$ . The order inequalities mean that $I - M$ and $I + M$ have nonnegative quadratic forms.

[F1]

Complex spectral theorem: a normal endomorphism of a finite-dimensional complex inner product space has an orthonormal eigenbasis, and conversely: a finite-dimensional normal operator has an orthonormal eigenbasis.

[F2]

The adjoint $T^{*} : W \to V$ is characterised by $⟨ T v, w ⟩_{W} = ⟨ v, T^{*} w ⟩_{V}$ and Real and complex inner-product spaces and their induced length: $⟨ M v, w ⟩ = ⟨ v, M^{*} w ⟩$ and the inner product is conjugate-symmetric.

[F3]

The spectral functional calculus f(T) for a normal endomorphism: if $M = \sum_{j} λ_{j} P_{j}$ , then $f (M) = \sum_{j} f (λ_{j}) P_{j}$ for $f$ on its spectrum.

[F4]

The real exponential function and the number $e$ by a power series and The exponential series converges absolutely for every real argument: $\exp (u) = \sum_{k \geq 0} u^{k} / k!$ , and this series converges absolutely for every real input, so consecutive tails may be grouped.

[F5]

The factorial $n!$ and the falling factorial $n^{\underline{k}}$ , defined by recursion in $N$ , Integer powers $a^{m}$ , and Monotonicity of $x \mapsto x^{n}$ and of $n \mapsto a^{n}$ : $(k + 1)! = (k + 1) k!$ , powers satisfy $a^{n + 1} = a^{n} a$ , and $0 \leq u \leq 1$ implies $u^{n} \leq 1$ .

[F6]

For $∣ r ∣ < 1$ , $\sum_{k \geq 0} r^{k} = 1 / (1 - r)$ , and for $∣ r ∣ \geq 1$ the series diverges: $\sum_{j \geq 0} 2^{- j} = 2$ .

[F7]

Non-negative and positive operators and Finite semidefinite primal-dual pair: nonnegative and positive-semidefinite operators have the stated quadratic-form meanings.

Proof

technique · direct

1.1givenF4F5F6algebra

Put $u = - η x$ , so $∣ u ∣ \leq 1$ . From [F5] and $2! = 2$ , induction gives $k! \geq 2^{k - 1}$ for $k \geq 2$ : if it holds at $k \geq 2$ , then $(k + 1)! = (k + 1) k! \geq 3 \cdot 2^{k - 1} > 2^{k}$ , so the bound is strict for $k \geq 3$ . Thus [F6] gives $\sum_{k \geq 2} 1 / k! \leq 1 / 2 + 1 / 6 + \sum_{k \geq 4} 2^{- (k - 1)} = 1 / 2 + 1 / 6 + (1 / 8) \sum_{j \geq 0} 2^{- j} = 11 / 12 < 1$ . If $u = 0$ , [F4] gives $\exp (u) = 1 = 1 + u + u^{2}$ . If $0 < u \leq 1$ , then $u^{k} = u^{2} u^{k - 2} \leq u^{2}$ for $k \geq 2$ by [F5], so [F4] gives $\exp (u) = 1 + u + \sum_{k \geq 2} u^{k} / k! \leq 1 + u + u^{2} \sum_{k \geq 2} 1 / k! < 1 + u + u^{2}$ . If $u = - v \leq 0$ with $0 \leq v \leq 1$ , the absolute convergence in [F4] allows consecutive grouping because the partial sums after each pair are a subsequence of the ordinary partial sums and hence have the same limit; each pair after the quadratic term is $- v^{2 j + 3} / (2 j + 3)! + v^{2 j + 4} / (2 j + 4)! = - \frac{v^{2 j + 3}}{(2 j + 3)!} (1 - \frac{v}{2 j + 4}) \leq 0$ for $j \geq 0$ . Hence $\exp (- v) \leq 1 - v + v^{2} / 2 \leq 1 - v + v^{2}$ . In every case, $\exp (u) \leq 1 + u + u^{2}$ .

2.1givenF1F2F3F7step 1.1algebra∎

The scalar bound in step 1.1 gives $\exp (- η x) \leq 1 - η x + η^{2} x^{2} \leq 1 - η x + η^{2}$ . Since $M = M^{*}$ , it is normal, so [F1] gives an orthonormal eigenbasis $M e_{k} = λ_{k} e_{k}$ . For each unit $e_{k}$ , [F2] gives $λ_{k} = ⟨ M e_{k}, e_{k} ⟩ = ⟨ e_{k}, M e_{k} ⟩ = \overline{λ_{k}}$ , hence $λ_{k}$ is real; testing the order bounds on $e_{k}$ gives $1 - λ_{k} \geq 0$ and $1 + λ_{k} \geq 0$ , so $λ_{k} \in [- 1, 1]$ . By [F3], $\exp (- η M)$ and $I - η M + η^{2} I$ are diagonal in this basis, and applying the scalar bound to each eigenvalue shows their difference is positive semidefinite by [F7].

Depends on

Used by

Dependency tree · two levels

72 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

https://arxiv.org/pdf/1705.01843v4 (standard reference, not scraped)