LemmaStatement: Literature-sourcedProof: 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.

Gradient steps of smooth convex functions are nonexpansive

Statement

Let $h : R^{d} \to R$ be convex and differentiable with $β$ -Lipschitz gradient, where $β > 0$ . For every $0 \leq η \leq 2 / β$ and $x, y \in R^{d}$ , $∥ x - y - η (\nabla h (x) - \nabla h (y)) ∥_{2} \leq ∥ x - y ∥_{2} .$

Statement references

Karimireddy et al., SCAFFOLD, Appendix C, Lemma 6 proves a related contraction for $μ$ -strongly convex functions with $η \leq 1 / β$ and squared-distance factor $1 - μ η$ . The convex-only nonexpansiveness for the full range $0 \leq η \leq 2 / β$ is established by the local proof below.

Facts & Assumptions

Given: The differentiable convex function and gradient step in the Statement.

[F1]

Convex and strictly convex functions on Euclidean convex sets: convexity means $h ((1 - t) u + t z) \leq (1 - t) h (u) + t h (z)$ for $u, z \in R^{d}$ and $t \in [0, 1]$ .

[F2]

Descent inequality for a Lipschitz gradient: a $β$ -Lipschitz gradient satisfies the quadratic descent inequality.

[F3]

The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ : inner products are bilinear and $∥ v ∥_{2}^{2} = ⟨ v, v ⟩$ .

Proof

1.1F1F2givenalgebra

Fix $u, v \in R^{d}$ . For every $z \in R^{d}$ and $0 < t \leq 1$ , [F1] gives [given] $\frac{h (u + t (z - u)) - h (u)}{t} \leq h (z) - h (u) .$ As $t ↓ 0$ , differentiability makes the left side tend to $⟨ \nabla h (u), z - u ⟩$ . Hence $h (z) \geq h (u) + ⟨ \nabla h (u), z - u ⟩$ . Define $ϕ (z) = h (z) - ⟨ \nabla h (u), z - u ⟩$ ; this inequality shows that $u$ minimizes $ϕ$ . Its gradient is $β$ -Lipschitz, hence continuous. Apply [F2] at $v$ to $v - β^{- 1} \nabla ϕ (v)$ and use $ϕ (u) \leq ϕ (z)$ to obtain $∥ \nabla h (v) - \nabla h (u) ∥_{2}^{2} \leq 2 β (h (v) - h (u) - ⟨ \nabla h (u), v - u ⟩) .$

2.1F3step 1.1givenalgebra

Repeat step 1.1 with $u$ and $v$ exchanged and add the two inequalities. [given] The right-hand Bregman terms sum to $⟨ \nabla h (v) - \nabla h (u), v - u ⟩$ , so $∥ \nabla h (v) - \nabla h (u) ∥_{2}^{2} \leq β ⟨ \nabla h (v) - \nabla h (u), v - u ⟩ .$

3.1F3step 2.1givenalgebra∎

Expand the square in the Statement and apply step 2.1: [given] $\begin{aligned} ∥ x - y - η (\nabla h (x) - \nabla h (y)) ∥_{2}^{2} & \leq ∥ x - y ∥_{2}^{2} - (\frac{2 η}{β} - η^{2}) ∥ \nabla h (x) - \nabla h (y) ∥_{2}^{2} \\ \leq ∥ x - y ∥_{2}^{2}, \end{aligned}$ because $0 \leq η \leq 2 / β$ . Taking nonnegative square roots proves the claim.

Depends on

Used by

Dependency tree · two levels

24 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

Sai Praneeth Karimireddy et al., SCAFFOLD, Appendix C, Lemma 6 (standard reference, not scraped)