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.

AMSGrad momentum energy is bounded by a coordinatewise weighted gradient sum

Statement

Run uncorrected AMSGrad for a finite horizon $T \geq 1$ with $α_{t} = α / \sqrt{t}$ , $α > 0$ , $β_{2} \in (0, 1)$ , $0 \leq β_{1, t} \leq β_{1} < \sqrt{β_{2}}$ , and $γ = β_{1} / \sqrt{β_{2}}$ . For each coordinate, interpret $m_{t, i}^{2} / \sqrt{{\hat{v}}_{t, i}}$ as zero when ${\hat{v}}_{t, i} = 0$ . Then $\sum_{t = 1}^{T} α_{t} \sum_{i = 1}^{d} \frac{m_{t, i}^{2}}{\sqrt{{\hat{v}}_{t, i}}} \leq \frac{α}{(1 - β_{1}) (1 - γ) \sqrt{1 - β_{2}}} \sum_{i = 1}^{d} \sum_{t = 1}^{T} \frac{∣ g_{t, i} ∣}{\sqrt{t}} .$

Statement references

Uncorrected AMSGrad with a coordinatewise historical maximum: gives the moment recurrences, historical maximum, and time-varying first-moment weights.

RMSProp, Adam, and AMSGrad moment updates are well-defined: all moment coordinates are finite and all second-moment coordinates are nonnegative; a zero second-moment coordinate has zero first moment.

Cauchy-Schwarz $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥_{2} ∥ y ∥_{2}$ with its equality case, the triangle inequality for $∥ \cdot ∥_{2}$ , the parallelogram law and polarisation: finite-coordinate Cauchy–Schwarz.

Reddi, Kale, and Kumar, Appendix D

Facts & Assumptions

Given: The finite gradient vectors and AMSGrad recurrences in the Statement, with the stated parameter ranges.

[F1]

Uncorrected AMSGrad with a coordinatewise historical maximum: $m_{t, i} = β_{1, t} m_{t - 1, i} + (1 - β_{1, t}) g_{t, i}$ and $v_{t, i} = β_{2} v_{t - 1, i} + (1 - β_{2}) g_{t, i}^{2}$ .

[F2]

RMSProp, Adam, and AMSGrad moment updates are well-defined: $0 \leq v_{t, i} \leq {\hat{v}}_{t, i}$ ; because $β_{2} > 0$ , $v_{t, i} = 0$ exactly when ${\hat{v}}_{t, i} = 0$ , and then all corresponding moment and gradient entries are zero.

[F3]

Cauchy-Schwarz $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥_{2} ∥ y ∥_{2}$ with its equality case, the triangle inequality for $∥ \cdot ∥_{2}$ , the parallelogram law and polarisation: for finite real lists, $(\sum_{j} a_{j} b_{j})^{2} \leq (\sum_{j} a_{j}^{2}) (\sum_{j} b_{j}^{2})$ .

[F4]

Integer powers $a^{m}$ , The natural numbers $N$ (von Neumann), Finite sums and finite products, by recursion, and Laws of finite sums and finite products: $β^{0} = 1$ , $β^{n + 1} = β^{n} β$ , finite sums distribute over addition, and finite sums may be reindexed.

[F5]

Squaring is monotone on the nonnegatives and Square roots exist: a unique $\sqrt{a} \geq 0$ with $(\sqrt{a})^{2} = a$ ; the positives are ${x^{2} : x \neq 0}$ : if $0 \leq a \leq b$ , then $\sqrt{a} \leq \sqrt{b}$ .

[F6]

Ordered field, Sign rules for products and monotonicity of multiplication, Inverses of positives are positive, and reciprocation reverses order, and The Cauchy-sequence reals have the least-upper-bound property: positive coefficients preserve inequalities and positive denominators may be divided through.

Proof

Given: The hypotheses in the Statement.

1.1F1F6giveninductionalgebra

Expanding the first-moment recurrence [F1] recursively gives $m_{t, i} = \sum_{j = 1}^{t} a_{t, j} g_{j, i}$ , where $a_{t, t} = 1 - β_{1, t}$ and $a_{t, j} = β_{1, t} a_{t - 1, j}$ for $j < t$ . Induction gives $0 \leq a_{t, j} \leq β_{1}^{t - j}$ : the terminal coefficient is at most $1$ , and each earlier coefficient acquires one factor at most $β_{1}$ .

2.1F3F4F5F6step 1.1givenalgebra

By [F3] applied to $\sqrt{a_{t, j}}$ and $\sqrt{a_{t, j}} g_{j, i}$ , $m_{t, i}^{2} \leq (\sum_{j = 1}^{t} a_{t, j}) (\sum_{j = 1}^{t} a_{t, j} g_{j, i}^{2}) \leq \frac{1}{1 - β_{1}} \sum_{j = 1}^{t} β_{1}^{t - j} g_{j, i}^{2},$ because $\sum_{k = 0}^{t - 1} β_{1}^{k} = (1 - β_{1}^{t}) / (1 - β_{1}) \leq 1 / (1 - β_{1})$ . The identity follows by multiplying the finite sum by $1 - β_{1}$ and telescoping $\sum_{k = 0}^{t - 1} (β_{1}^{k} - β_{1}^{k + 1}) = 1 - β_{1}^{t}$ using [F4]; the denominator is positive by [F6].

3.1F1F2F5F6step 2.1giveninductionalgebra

Iterating the second-moment recurrence [F1] gives $v_{t, i} = (1 - β_{2}) \sum_{j = 1}^{t} β_{2}^{t - j} g_{j, i}^{2}$ . By [F2] and [F5], $\sqrt{{\hat{v}}_{t, i}} \geq \sqrt{v_{t, i}}$ . If this value is zero, [F2] makes the energy term zero. Otherwise, for each nonzero $g_{j, i}$ , $\sqrt{v_{t, i}} \geq \sqrt{1 - β_{2}} \sqrt{β_{2}^{t - j}} ∣ g_{j, i} ∣ .$ The root recursion gives $\sqrt{β_{2}^{n}} = (\sqrt{β_{2}})^{n}$ for every integer $n \geq 0$ ; induction proves this because both sides are nonnegative and have the same square. Also $β_{1}^{n} / (\sqrt{β_{2}})^{n} = (β_{1} / \sqrt{β_{2}})^{n}$ by the integer-power recursion, so $β_{1}^{n} / \sqrt{β_{2}^{n}} = γ^{n}$ . Using step 2.1 termwise in the finite sum therefore gives $\frac{m_{t, i}^{2}}{\sqrt{{\hat{v}}_{t, i}}} \leq \frac{1}{(1 - β_{1}) \sqrt{1 - β_{2}}} \sum_{j = 1}^{t} γ^{t - j} ∣ g_{j, i} ∣ .$ Zero gradient terms contribute zero.

4.1F4F6step 2.1step 3.1givenalgebra∎

Multiply step 3.1 by $α / \sqrt{t}$ , sum over $t$ and coordinates, and reorder the finite sums. Since $1 / \sqrt{t} \leq 1 / \sqrt{j}$ for $t \geq j$ and $(1 - γ) \sum_{k = 0}^{T - j} γ^{k} = 1 - γ^{T - j + 1} \leq 1$ by the same finite telescoping identity from step 2.1, $\sum_{t = 1}^{T} α_{t} \sum_{i} \frac{m_{t, i}^{2}}{\sqrt{{\hat{v}}_{t, i}}} \leq \frac{α}{(1 - β_{1}) \sqrt{1 - β_{2}}} \sum_{i} \sum_{j = 1}^{T} ∣ g_{j, i} ∣ \sum_{t = j}^{T} \frac{γ^{t - j}}{\sqrt{t}} \leq \frac{α}{(1 - β_{1}) (1 - γ) \sqrt{1 - β_{2}}} \sum_{i} \sum_{j = 1}^{T} \frac{∣ g_{j, i} ∣}{\sqrt{j}} .$ This is the stated inequality.

Depends on

Used by

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

Dependency tree · two levels

64 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)