ExampleConstruction: Literature-sourcedVerification: 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.

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.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

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