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.
The projected OGD bound does not cover infeasible comparators
Statement refuted
Refuted claim: For integers , let be nonempty, closed, and convex with diameter at most a finite . Let each be differentiable and convex on an open convex neighborhood of , and suppose the projected online-gradient algorithm starts at , uses for finite , and has on every round. Assume Countable Choice for the metric projections. The refuted claim is that
holds for every comparator , including points outside .
Statement references
Projected online gradient descent has static regret at most three-halves of DG square-root T: its stated comparator belongs to .
Facts & Assumptions
Given: The projected OGD algorithm, , diameter bound , horizon , losses defined by for , initial point , gradient bound , and infeasible comparator .
The Axiom of Countable Choice (): Countable Choice is assumed for the nondegenerate projection updates.
Projected online gradient descent: and when .
The Euclidean inner product on : in , .
The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement: a set is closed when its complement is open.
The Jacobian matrix of partial derivatives and the gradient in the scalar-valued case: the gradient of a scalar-valued differentiable function on is its ordinary derivative.
Metric projection onto a closed convex set satisfies the variational inequality: exactly when for every .
Convex and strictly convex functions on Euclidean convex sets: a function is convex when it lies below the chord between any two points of its convex domain.
Projection onto a nonempty closed convex set: under Countable Choice, the metric projection onto exists and is unique.
Counterexample
The interval is nonempty. For and , , so [F3] makes it convex. Its complement is . If , the ball of radius about lies in ; if , the ball of radius about lies in . Thus [F4] makes closed. Its diameter is because for and the endpoints attain distance .
For each and , , so the derivative is by [F5]; the affine identity and [F7] show convexity. Also .
By [A1] and [F8], both metric projections exist uniquely. Since , and . The first unprojected point is ; for every , , so [F6] gives . The next unprojected point is ; for every , , so [F6] gives .
The learner's two played losses sum to , whereas the infeasible comparator has . Its regret is therefore .
The proposed right-hand side is , since . Thus the regret inequality fails for .
Depends on
- Projected online gradient descent
- Projected online gradient descent has static regret at most three-halves of DG square-root T
- The Euclidean inner product $\langle x,y\rangle = \sum_{k<n} x_k y_k$ on $\mathbb{R}^n$
- The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement
- Intervals of $\mathbb{R}$: the nine order-convex forms, nondegeneracy, and length
- A convex subset of $\mathbb{R}^m$ contains every line segment between two of its points
- Convex and strictly convex functions on Euclidean convex sets
- The Jacobian matrix of partial derivatives and the gradient in the scalar-valued case
- Projection onto a nonempty closed convex set
- Metric projection onto a closed convex set satisfies the variational inequality
- The Axiom of Countable Choice ($\mathrm{AC}_\omega$)
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
57 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)
- Tengyu Ma, Lecture Notes for Machine Learning Theory, Chapter 11 (standard reference, not scraped)