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.

AdaGrad with a singular diagonal metric

Example

Use the diagonal AdaGrad scale in dimension $2$ with $K = [- 1, 1]^{2}$ , $x_{1} = (0, 0)$ , one round, step size $η = 1$ , and supplied gradient $g_{1} = (1, 0)$ . Then $G_{1} = H_{1} = diag (1, 0)$ , $H_{1}^{†} = diag (1, 0)$ , and $y_{2} = (- 1, 0)$ . For a decision vector $(a, b) \in K$ , the metric projection objective is $(a + 1)^{2}$ , so its minimizers are all points $(- 1, s)$ with $s \in [- 1, 1]$ . In particular, one may select $x_{2} = (- 1, 0)$ . The metric is singular and the projection is nonunique.

Example references

Gram-matrix AdaGrad with full or singular diagonal metrics: defines the diagonal scale, pseudoinverse update, and metric projection used in this calculation.

A singular AdaGrad metric still has a projection minimizer: proves that the projection objective has a minimizer even for a singular metric.

The diagonal AdaGrad scale is the coordinatewise square root: identifies the diagonal scale entry with the square root of accumulated squared coordinate gradients.

The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ : the coordinates use the standard Euclidean inner product.

The Moore--Penrose pseudoinverse $A^{+}$ as the solution of the four Penrose equations: characterizes the pseudoinverse by four matrix equations.

Facts & Assumptions

Given: The one-round update data in the Example.

[F1]

Gram-matrix AdaGrad with full or singular diagonal metrics: $G_{1} = g_{1} g_{1}^{⊤}$ , $H_{1} = diag (\sqrt{(G_{1})_{11}}, \sqrt{(G_{1})_{22}})$ , $y_{2} = x_{1} - η H_{1}^{†} g_{1}$ , and $x_{2}$ minimizes $(x - y_{2})^{⊤} H_{1} (x - y_{2})$ on $K$ .

[F2]

The diagonal AdaGrad scale is the coordinatewise square root: $(H_{1})_{i i} = \sqrt{g_{1, i}^{2}}$ .

[F3]

The Moore--Penrose pseudoinverse $A^{+}$ as the solution of the four Penrose equations: $B$ is the Moore–Penrose pseudoinverse of $A$ when $A B A = A$ , $B A B = B$ , and $A B$ and $B A$ are self-adjoint.

[F4]

A singular AdaGrad metric still has a projection minimizer: the quadratic objective attains a minimum on nonempty bounded closed $K$ , even if $H_{1}$ is singular.

Verification

1.1givenF1F2F3algebra

The outer product is $G_{1} = g_{1} g_{1}^{⊤} = (\begin{array}{cc} 1 & 0 \\ 0 & 0 \end{array})$ . By [F1, F2], $H_{1} = diag (1, 0)$ ; the matrix $D = diag (1, 0)$ satisfies $H_{1} D H_{1} = H_{1}$ , $D H_{1} D = D$ , and both $H_{1} D$ and $D H_{1}$ equal the symmetric matrix $D$ . By [F3], $H_{1}^{†} = D$ .

2.1step 1.1F1algebra

The update gives $y_{2} = (0, 0) - diag (1, 0) (1, 0) = (- 1, 0)$ . For $(a, b) \in [- 1, 1]^{2}$ , $((a, b) - y_{2})^{⊤} H_{1} ((a, b) - y_{2}) = (a + 1)^{2}$ , which is minimized exactly when $a = - 1$ , with $b$ arbitrary in $[- 1, 1]$ .

3.1step 2.1F4algebra∎

Hence the entire minimizer set is ${(- 1, s) : s \in [- 1, 1]}$ , containing distinct points, and the selected $x_{2} = (- 1, 0)$ is valid. The metric has a zero eigenvalue, and [F4] independently guarantees existence of at least one minimizer.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

32 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

Elad Hazan, Introduction to Online Convex Optimization, second edition (standard reference, not scraped)
John Duchi, Elad Hazan, and Yoram Singer, Adaptive Subgradient Methods for Online Learning and Stochastic Optimization (standard reference, not scraped)