Pipeline-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.

Adaptive gradient algorithms and regret limits — Examples

1 · Prerequisites

2 · Logical flowchart

3 · Definitions, theorems and proofs

None yet.

4 · Examples, counterexamples and false statements

ExampleConstruction: Literature-sourcedVerification: AI-adaptedOpen item page →

A fixed denominator regularizer does not prevent Adam's periodic regret example

Example

Fix $ϵ > 0$ . On $[- 1, 1]$ , run the uncorrected scalar Adam update with $α = 1 / 10$ , $β_{1} = 0$ , $β_{2} = 1 / 45$ , $x_{1} = 1$ , and denominator $\sqrt{v_{t} + ϵ}$ . Repeat the losses $ℓ_{3 k + 1} (x) = 3 \sqrt{ϵ} x$ and $ℓ_{3 k + 2} (x) = ℓ_{3 k + 3} (x) = - \sqrt{ϵ} x$ for every integer $k \geq 0$ , feeding their slopes as the algorithm's gradients. The best-comparator regret has limit inferior average at least $2 \sqrt{ϵ} / 3$ .

Example references

Uncorrected Adam for online convex losses: fixes the scalar update, inside-root denominator, and clipping convention.

Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length: $[- 1, 1]$ is the closed interval used as the domain.

Adam can have nonzero average regret on a one-dimensional convex sequence: proves the positive-epsilon periodic construction and its average-regret lower bound.

Reddi, Kale, and Kumar, Appendix F

Facts & Assumptions

Given: The fixed positive $ϵ$ and periodic losses in the Example.

[F1]

Uncorrected Adam for online convex losses: the second moment is $v_{t} = β_{2} v_{t - 1} + (1 - β_{2}) g_{t}^{2}$ , the denominator is $\sqrt{v_{t} + ϵ}$ , and the iterate is clipped to $[- 1, 1]$ .

[F2]

RMSProp, Adam, and AMSGrad moment updates are well-defined: for every finite admissible run, the moments are finite, the second moments are nonnegative, and every specified denominator is positive.

[F3]

Adam can have nonzero average regret on a one-dimensional convex sequence: for every $ϵ > 0$ , the parameters $α = 1 / 10$ , $β_{1} = 0$ , $β_{2} = 1 / 45$ , and the displayed period yield ${lim inf}_{T \to \infty} R_{T} / T \geq 2 \sqrt{ϵ} / 3$ .

[F4]

Convex and strictly convex functions on Euclidean convex sets and A convex subset of $R^{m}$ contains every line segment between two of its points: $[- 1, 1]$ is convex and every displayed linear loss is convex on it.

[F5]

The principle of mathematical induction and Ordered field: induction applies to the moment recurrences, and sums and products of nonnegative reals are nonnegative.

Verification

Given: $ϵ > 0$ and the stated scalar run.

1.1F1F2F4F5giveninductionalgebra

Each gradient is finite and $g_{t}^{2} \in {9 ϵ, ϵ}$ . Starting from $v_{0} = 0$ , induction in the recurrence $v_{t} = v_{t - 1} / 45 + 44 g_{t}^{2} / 45$ gives finite $v_{t} \geq 0$ by [F1] and [F5]. Hence $v_{t} + ϵ > 0$ at every round, so its square root is positive; with $m_{t} = g_{t}$ and clipping to $[- 1, 1]$ , the update defines an admissible run at every finite horizon. Thus [F2] applies after admissibility has been established. For $x, y \in [- 1, 1]$ and $θ \in [0, 1]$ , every loss satisfies $ℓ_{t} ((1 - θ) x + θ y) = (1 - θ) ℓ_{t} (x) + θ ℓ_{t} (y)$ , so it is convex by [F4].

2.1F3step 1.1given∎

The positive-epsilon case of [F3] has exactly these parameters, initialization, denominator placement, clipping rule, and period of losses. Its conclusion gives the claimed limit inferior average regret.

ExampleConstruction: Literature-sourcedVerification: AI-adaptedjudge pass (gpt-6-luna)Open item page →

AMSGrad retains an earlier second-moment maximum

Example

On the one-dimensional domain $F = [- 1, 1]$ , run uncorrected AMSGrad from $x_{1} = 0$ with positive step sizes $α_{1}, α_{2}$ , any first-moment weights in $[0, 1)$ , $β_{2} = 1 / 2$ , and losses $ℓ_{1} (x) = 2 x$ , $ℓ_{2} (x) = 0$ , using their gradients $g_{1} = 2$ , $g_{2} = 0$ . The raw second moment decreases from $v_{1} = 2$ to $v_{2} = 1$ , while the historical maximum remains ${\hat{v}}_{1} = {\hat{v}}_{2} = 2$ .

Example references

Uncorrected AMSGrad with a coordinatewise historical maximum: defines the raw second-moment recurrence and its coordinatewise historical maximum.

Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length: $[- 1, 1]$ is the closed interval used as the domain.

RMSProp, Adam, and AMSGrad moment updates are well-defined: guarantees finite nonnegative moments and well-defined updates on the stated compact domain.

Reddi, Kale, and Kumar, Algorithm 2

Facts & Assumptions

Given: $F = [- 1, 1]$ , $x_{1} = 0$ , $β_{2} = 1 / 2$ , and gradients $g_{1} = 2$ , $g_{2} = 0$ .

[F1]

Uncorrected AMSGrad with a coordinatewise historical maximum: $v_{0} = {\hat{v}}_{0} = 0$ , $v_{t} = β_{2} v_{t - 1} + (1 - β_{2}) g_{t}^{2}$ , and ${\hat{v}}_{t} = \max {{\hat{v}}_{t - 1}, v_{t}}$ .

[F2]

RMSProp, Adam, and AMSGrad moment updates are well-defined: the recurrence and weighted minimizations are well-defined for finite gradients on the nonempty compact convex domain.

[F3]

Convex and strictly convex functions on Euclidean convex sets and A convex subset of $R^{m}$ contains every line segment between two of its points: the interval is convex and the linear losses are convex.

[F4]

Subgradients and the subdifferential of a convex function: $g \in \partial ℓ (x)$ when $ℓ (y) \geq ℓ (x) + g (y - x)$ for all $y$ in the domain.

[F5]

Ordered field and Sign rules for products and monotonicity of multiplication: nonnegative coefficients preserve the interval bounds under weighted sums.

[F6]

For a nonempty subset of $R^{n}$ with $n \geq 1$ , compactness, closedness and boundedness, pseudocompactness, and attainment of extrema by every continuous real-valued function are equivalent: a nonempty closed bounded subset of $R$ is compact.

Verification

Given: The initialization and two gradients in the Example.

1.1F1F2F3F4F5F6givenalgebra

The interval $[- 1, 1]$ is nonempty, closed, and bounded, so [F6] makes it compact. For $x, y \in [- 1, 1]$ and $θ \in [0, 1]$ , [F5] gives $- 1 \leq (1 - θ) x + θ y \leq 1$ , so the interval is convex. For either displayed linear loss, $ℓ ((1 - θ) x + θ y) = (1 - θ) ℓ (x) + θ ℓ (y)$ ; moreover, if $ℓ (x) = a x$ , its gradient $g = a$ satisfies $ℓ (y) = ℓ (x) + g (y - x)$ , so it is a subgradient by [F4]. The first update gives $v_{1} = (1 / 2) 0 + (1 / 2) 2^{2} = 2$ and ${\hat{v}}_{1} = \max {0, 2} = 2$ .

2.1F1F3F4step 1.1givenalgebra∎

The second update gives $v_{2} = (1 / 2) 2 + (1 / 2) 0^{2} = 1$ , so $v_{2} < v_{1}$ ; nevertheless ${\hat{v}}_{2} = \max {2, 1} = 2 = {\hat{v}}_{1}$ .

ExampleConstruction: Literature-sourcedVerification: AI-adaptedjudge pass (gpt-6-luna)Open item page →

Constant first-moment weight is outside the proved square-root regret schedule

Example

Let $F = [- 1, 1]$ , $x_{1} = 0$ , $ℓ_{t} (x) = x$ , $g_{t} = 1$ , $α_{t} = 1 / \sqrt{t}$ , $β_{1, t} = 1 / 4$ for every round, and $β_{2} = 1 / 2$ . The hypotheses of the AMSGrad regret inequality hold, but the second, first-moment correction term in its displayed bound is at least $4 T^{3 / 2} / 9$ for $T \geq 2$ . This shows that the bound does not give an $O (\sqrt{T})$ guarantee for this constant schedule; it gives no lower bound on the algorithm's actual regret.

Example references

AMSGrad has an online convex regret bound under decaying first-moment weights: gives the regret inequality and states the geometric and reciprocal first-moment schedules for its $O (\sqrt{T})$ consequence.

Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length: $[- 1, 1]$ is the closed interval used as the feasible domain.

Uncorrected AMSGrad with a coordinatewise historical maximum: defines the raw moment recurrence used to calculate the correction term.

Reddi, Kale, and Kumar, Theorem 4 and Corollary 1

Facts & Assumptions

Given: The domain, losses, gradients, and parameters in the Example.

[F1]

Uncorrected AMSGrad with a coordinatewise historical maximum: $v_{0} = 0$ and $v_{t} = β_{2} v_{t - 1} + (1 - β_{2}) g_{t}^{2}$ , with ${\hat{v}}_{t} = \max {{\hat{v}}_{t - 1}, v_{t}}$ .

[F2]

AMSGrad has an online convex regret bound under decaying first-moment weights: under its stated domain, loss, gradient, and parameter hypotheses, the second correction term is $\frac{D_{\infty}^{2}}{(1 - β_{1})^{2}} \sum_{t = 1}^{T} \frac{β_{1, t} \sqrt{{\hat{v}}_{t}}}{α_{t}} .$

[F3]

Convex and strictly convex functions on Euclidean convex sets and A convex subset of $R^{m}$ contains every line segment between two of its points: convexity means $f ((1 - θ) x + θ y) \leq (1 - θ) f (x) + θ f (y)$ on a convex set, for $θ \in [0, 1]$ .

[F4]

Absolute value in an ordered field, Basic properties of the absolute value, Continuity of a map between metric spaces, at a point and globally, in the $ε$ - $δ$ form, and The absolute value makes $R$ a metric space: $d (x, y) = ∣ x - y ∣$ is a metric, its open balls are the intervals $(x - r, x + r)$ , and it is unbounded: continuity on $R$ is checked with the usual distance $∣ x - y ∣$ and the $ε$ - $δ$ criterion.

[F5]

[F6]

Subgradients and the subdifferential of a convex function: $g \in \partial f (x)$ when $f (y) \geq f (x) + g (y - x)$ for all $y$ in the domain.

[F7]

Every complete ordered field is Archimedean: the positive integers are unbounded, so the growth estimates below are unbounded as $T$ increases.

[F8]

Ordered field and Sign rules for products and monotonicity of multiplication: nonnegative coefficients preserve interval bounds under weighted sums.

[F9]

Intervals of $R$ : the nine order-convex forms, nondegeneracy, and length: $[- 1, 1]$ is the closed interval with endpoints $- 1$ and $1$ .

Verification

Given: The one-dimensional online run in the Example.

1.1F1F2F3F4F5F6F8F9giveninductionalgebra

The interval $[- 1, 1]$ is nonempty, closed, and bounded by [F9], hence compact by [F5]. For $x, y \in [- 1, 1]$ and $θ \in [0, 1]$ , [F8] gives $- 1 \leq (1 - θ) x + θ y \leq 1$ , so the domain is convex. Also $ℓ_{t} ((1 - θ) x + θ y) = (1 - θ) ℓ_{t} (x) + θ ℓ_{t} (y)$ , so each loss is convex by [F3]. Since $∣ ℓ_{t} (x) - ℓ_{t} (y) ∣ = ∣ x - y ∣$ , choosing $δ = η$ in [F4] proves continuity for every tolerance $η > 0$ . The gradient $g_{t} = 1$ is a subgradient because $ℓ_{t} (y) = ℓ_{t} (x) + (y - x)$ by [F6], and $γ = β_{1} / \sqrt{β_{2}} = \sqrt{2} / 4 < 1$ . Thus the hypotheses for [F2] hold. Iterating [F1] gives $v_{t} = 1 - 2^{- t}$ , which is nondecreasing, so ${\hat{v}}_{t} = v_{t} \geq 1 / 2$ for every $t \geq 1$ .

2.1F2F4step 1.1givenalgebra

Here $α_{t} = 1 / \sqrt{t}$ and $β_{1, t} = 1 / 4$ . The second term in [F2] is therefore at least $\frac{4}{(3 / 4)^{2}} \sum_{t = 1}^{T} \frac{1}{4 \sqrt{2}} \sqrt{t} = \frac{16}{9 \sqrt{2}} \sum_{t = 1}^{T} \sqrt{t} .$ For $T \geq 2$ , at least $T / 2$ indices satisfy $t \geq T / 2$ , so $\sum_{t = 1}^{T} \sqrt{t} \geq T^{3 / 2} / (2 \sqrt{2})$ . The correction term is at least $4 T^{3 / 2} / 9$ .

3.1F2F7step 2.1givenalgebra∎

The constant schedule is neither $β_{1, t} = β_{1} λ^{t - 1}$ with $λ < 1$ nor $β_{1, t} = β_{1} / t$ . Since the theorem's upper-bound expression contains this positive term, that expression cannot be $O (\sqrt{T})$ for this schedule: dividing its lower bound by $\sqrt{T}$ gives $4 T / 9$ , which is unbounded by [F7]. The computation concerns the stated bound only and gives no lower bound on actual regret.

Adaptive gradient algorithms and regret limits — Examples

2 · Logical flowchart

3 · Definitions, theorems and proofs

4 · Examples, counterexamples and false statements

A fixed denominator regularizer does not prevent Adam's periodic regret example

Example

Example references

Facts & Assumptions

Verification

AMSGrad retains an earlier second-moment maximum

Example

Example references

Facts & Assumptions

Verification

Constant first-moment weight is outside the proved square-root regret schedule

Example

Example references

Facts & Assumptions

Verification

Sources