Alphabeta MathHow 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.
Cocoercive gradient bound for a convex smooth finite sum
Statement
Let n,d>=1, L>0, and let f_i:R^d->R be continuously differentiable, convex, with L-Lipschitz gradients. Put F=n^{-1}sum_i f_i. For all x,y in R^d,
Facts & Assumptions
Given: n,d>=1, L>0, the functions and regularity assumptions in the Statement, and the finite-sum convention of Finite sums and finite products, by recursion.
Descent inequality for a Lipschitz gradient: an L-Lipschitz gradient gives f(z)<=f(w)+<grad f(w),z-w>+(L/2)||z-w||_2^2 for all w,z.
Differentiable convex functions are characterized by the gradient inequality: a differentiable convex function satisfies f(z)>=f(w)+<grad f(w),z-w>.
Lipschitz map, -Hölder map for rational , and contraction: L-Lipschitz means ||grad f_i(a)-grad f_i(b)||_2<=L||a-b||_2.
Gradient of a finite sum is the finite sum of gradients: grad F(y)=n^{-1}sum_i grad f_i(y).
The Euclidean inner product on : ||z||_2^2=<z,z>, and the inner product is linear in each variable.
Convex and strictly convex functions on Euclidean convex sets: convexity is the segment inequality for values of the function.
Laws of finite sums and finite products: finite sums are additive and scale linearly.
Proof
Given: The objects and hypotheses in the Statement.
Fix i and y, and define h_i(z)=f_i(z)-<grad f_i(y),z>. Substituting this expression into the segment inequality [F6] shows that subtracting this linear function preserves convexity, and grad h_i(y)=0. By [F2] applied at y, h_i(z)>=h_i(y) for every z, so y is a global minimizer of h_i.
Apply [F1] to h_i at x and z=x-grad h_i(x)/L. Since subtracting a linear function leaves gradient differences unchanged, h_i is still L-smooth; substitution and algebra give h_i(z)<=h_i(x)-||grad h_i(x)||_2^2/(2L). Step 1.1 gives h_i(y)<=h_i(z), hence ||grad f_i(x)-grad f_i(y)||_2^2<=2L(f_i(x)-f_i(y)-<grad f_i(y),x-y>).
Sum the step 2.1 inequalities over i and divide by n. By [F4], grad F(y)=n^{-1}sum_i grad f_i(y); additivity and scaling [F7] identify the right side with 2L(F(x)-F(y)-<grad F(y),x-y>).
Depends on
- Finite sums and finite products, by recursion
- The Euclidean inner product $\langle x,y\rangle = \sum_{k<n} x_k y_k$ on $\mathbb{R}^n$
- Convex and strictly convex functions on Euclidean convex sets
- Lipschitz map, $\alpha$-Hölder map for rational $0 < \alpha \le 1$, and contraction
- Descent inequality for a Lipschitz gradient
- Differentiable convex functions are characterized by the gradient inequality
- Gradient of a finite sum is the finite sum of gradients
- Laws of finite sums and finite products
Used by
Dependency tree · two levels
50 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
- Rie Johnson and Tong Zhang, Accelerating Stochastic Gradient Descent using Predictive Variance Reduction, NeurIPS 2013 (standard reference, not scraped)
- Sébastien Bubeck, Convex Optimization: Algorithms and Complexity, complete monograph (standard reference, not scraped)