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.
RMSProp with an exponential second-moment estimate
Definition
Fix a dimension , an initial vector , a finite or infinite sequence of finite gradient vectors , positive step sizes , a decay parameter , and a denominator constant . Use one-based coordinate notation for every vector and . Set . At each integer round , update the second-moment estimate coordinatewise by
and then set
For a finite gradient sequence of length , perform rounds and return the trajectory ; when , return . For an infinite gradient sequence, perform every round , thereby defining and returning the iterate sequence . The root, addition, and division in the update are coordinatewise. The procedure makes no convergence or regret claim.
Definition references
The Euclidean inner product on : vectors in have the stated real coordinates, and vector updates are interpreted coordinatewise.
Squares of nonzero elements are positive: every nonzero squared gradient coordinate is positive.
Multiplication by zero: : a zero gradient coordinate has square zero.
Square roots exist: a unique with ; the positives are : each nonnegative real has a unique nonnegative square root.
Sign rules for products and monotonicity of multiplication: the decay coefficients and their complements are nonnegative, so the moment recurrence preserves nonnegativity.
Remarks
This is the no-momentum RMSProp variant with a positive constant added outside the square root. It has no bias correction and defines only an update procedure.
Depends on
- The Euclidean inner product $\langle x,y\rangle = \sum_{k<n} x_k y_k$ on $\mathbb{R}^n$
- Square roots exist: a unique $\sqrt{a} \ge 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
- The Cauchy-sequence reals have the least-upper-bound property
Used by
Dependency tree · two levels
30 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
- Léon Bottou, Frank E. Curtis, and Jorge Nocedal, Optimization Methods for Large-Scale Machine Learning (standard reference, not scraped)
- Sashank J. Reddi, Satyen Kale, and Sanjiv Kumar, On the Convergence of Adam and Beyond (standard reference, not scraped)