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.

One-step regret inequality for AMSGrad

Statement

At an AMSGrad round, let $F \subseteq R^{d}$ be nonempty, compact, and convex, let $x_{t}, x_{t + 1} \in F$ , let $ℓ_{t} : F \to R$ be convex, and let $g_{t} \in \partial ℓ_{t} (x_{t})$ . Take $α_{t} > 0$ and $β_{1, t} \in [0, 1)$ . Write $q_{t, i} = \sqrt{{\hat{v}}_{t, i}}$ , $Q_{t} = diag (q_{t, 1}, \dots, q_{t, d})$ , and $∥ z ∥_{Q_{t}}^{2} : = \sum_{i} q_{t, i} z_{i}^{2}, E_{t} (z) : = \sum_{i : q_{t, i} > 0} \frac{z_{i}^{2}}{q_{t, i}},$ with zero contribution from coordinates where $q_{t, i} = 0$ . For the AMSGrad update, every such zero coordinate has $m_{t, i} = m_{t - 1, i} = 0$ . Then for every comparator $u \in F$ , $ℓ_{t} (x_{t}) - ℓ_{t} (u) \leq \frac{∥ x_{t} - u ∥_{Q_{t}}^{2} - ∥ x_{t + 1} - u ∥_{Q_{t}}^{2}}{2 α_{t} (1 - β_{1, t})} + \frac{α_{t}}{2 (1 - β_{1, t})} E_{t} (m_{t}) + \frac{β_{1, t} α_{t}}{2 (1 - β_{1, t})} E_{t} (m_{t - 1}) + \frac{β_{1, t}}{2 α_{t} (1 - β_{1, t})} ∥ x_{t} - u ∥_{Q_{t}}^{2} .$

Statement references

Uncorrected AMSGrad with a coordinatewise historical maximum: defines the raw-moment recurrence, weighted minimization, and zero-coordinate convention.

RMSProp, Adam, and AMSGrad moment updates are well-defined: zero historical maximum implies zero current and previous first moments.

Subgradients and the subdifferential of a convex function: a subgradient gives the supporting inequality for the loss.

Cauchy-Schwarz $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥_{2} ∥ y ∥_{2}$ with its equality case, the triangle inequality for $∥ \cdot ∥_{2}$ , the parallelogram law and polarisation: Cauchy–Schwarz and the Euclidean norm identities used in the weighted Young bound.

Reddi, Kale, and Kumar, Appendix D

Facts & Assumptions

Given: The AMSGrad state and update, a convex loss, a subgradient at $x_{t}$ , a comparator $u \in F$ , and $α_{t} > 0$ , $β_{1, t} \in [0, 1)$ .

[F1]

Uncorrected AMSGrad with a coordinatewise historical maximum: $m_{t, i} = β_{1, t} m_{t - 1, i} + (1 - β_{1, t}) g_{t, i}$ , and $x_{t + 1}$ minimizes the weighted squared distance from the specified $y_{t + 1}$ .

[F2]

RMSProp, Adam, and AMSGrad moment updates are well-defined: $Q_{t}$ has finite nonnegative diagonal entries; if $q_{t, i} = 0$ , then $m_{t, i} = m_{t - 1, i} = 0$ .

[F3]

Subgradients and the subdifferential of a convex function: $ℓ_{t} (x_{t}) - ℓ_{t} (u) \leq ⟨ g_{t}, x_{t} - u ⟩$ .

[F4]

The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ : the inner product and squared weighted norms are finite coordinate sums.

[F5]

Cauchy-Schwarz $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥_{2} ∥ y ∥_{2}$ with its equality case, the triangle inequality for $∥ \cdot ∥_{2}$ , the parallelogram law and polarisation: $∣ ⟨ a, b ⟩ ∣ \leq ∥ a ∥_{2} ∥ b ∥_{2}$ ; in particular the finite weighted-coordinate form follows by applying it to $a_{i} = m_{t - 1, i} / \sqrt{q_{t, i}}$ and $b_{i} = \sqrt{q_{t, i}} (x_{t, i} - u_{i})$ on positive-weight coordinates.

[F6]

A convex subset of $R^{m}$ contains every line segment between two of its points, Square roots exist: a unique $\sqrt{a} \geq 0$ with $(\sqrt{a})^{2} = a$ ; the positives are ${x^{2} : x \neq 0}$ , Squares of nonzero elements are positive, Multiplication by zero: $0 \cdot a = 0$ , Ordered field, Sign rules for products and monotonicity of multiplication, and Inverses of positives are positive, and reciprocation reverses order: segments between feasible points remain feasible; nonnegative coordinates have nonnegative roots; weighted squares are nonnegative; and division by a positive denominator preserves the displayed inequalities.

Proof

Given: The state, update, convex loss, subgradient, comparator, and positive step size in the Statement.

1.1F1F2F4F6givenalgebra

Put $y_{i} = x_{t, i} - α_{t} m_{t, i} / q_{t, i}$ when $q_{t, i} > 0$ and $y_{i} = x_{t, i}$ otherwise. Let $p = x_{t + 1}$ , $D = ∥ u - p ∥_{Q_{t}}^{2} \geq 0$ , and $c = \sum_{i} q_{t, i} (p_{i} - y_{i}) (u_{i} - p_{i})$ . Convexity of $F$ makes $p + s (u - p) \in F$ for $0 < s \leq 1$ . Minimality of $p$ gives $0 \leq 2 s c + s^{2} D$ . If $c < 0$ , set $a = - c > 0$ and $s = a / (D + a + 1)$ ; then $0 < s < 1$ and $s D < a$ , so $2 s c + s^{2} D = s (- 2 a + s D) < - s a < 0$ , a contradiction. Thus $c \geq 0$ , and expansion of $∥ u - y ∥_{Q_{t}}^{2}$ yields $∥ p - u ∥_{Q_{t}}^{2} \leq ∥ y - u ∥_{Q_{t}}^{2}$ .

2.1F1F2F4F6step 1.1givenalgebra

Expanding the right side from step 1.1 and using $m_{t, i} = 0$ whenever $q_{t, i} = 0$ gives $⟨ m_{t}, x_{t} - u ⟩ \leq \frac{∥ x_{t} - u ∥_{Q_{t}}^{2} - ∥ x_{t + 1} - u ∥_{Q_{t}}^{2}}{2 α_{t}} + \frac{α_{t}}{2} E_{t} (m_{t}) .$ This follows coordinatewise from $y_{i} = x_{t, i} - α_{t} m_{t, i} / q_{t, i}$ on positive weights; zero-weight coordinates contribute zero.

3.1F1F2F3F5F6step 2.1givenalgebra∎

Rearranging the first-moment recurrence in [F1] gives $⟨ g_{t}, x_{t} - u ⟩ = \frac{⟨ m_{t}, x_{t} - u ⟩ - β_{1, t} ⟨ m_{t - 1}, x_{t} - u ⟩}{1 - β_{1, t}} .$ By [F2] zero-weight coordinates vanish; by [F5], weighted Cauchy–Schwarz on positive weights gives $∣ ⟨ m_{t - 1}, x_{t} - u ⟩ ∣ \leq E_{t} (m_{t - 1})^{1 / 2} ∥ x_{t} - u ∥_{Q_{t}}$ . For nonnegative $a, b$ , $0 \leq (\sqrt{α_{t}} a - b / \sqrt{α_{t}})^{2}$ expands to $a b \leq (α_{t} a^{2} + b^{2} / α_{t}) / 2$ , which bounds the negative cross term. Substituting step 2.1 and the subgradient inequality [F3] gives the stated four terms.

Depends on

Used by

AMSGrad has an online convex regret bound under decaying first-moment weights Theorem

Dependency tree · two levels

42 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

Sashank J. Reddi, Satyen Kale, and Sanjiv Kumar, On the Convergence of Adam and Beyond (standard reference, not scraped)