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.

Convex SCAFFOLD control-lag recursion

Statement

Let $f_{i} : R^{d} \to R$ be convex, differentiable and $β$ -smooth, with $f = N^{- 1} \sum_{i} f_{i}$ minimized at $x^{⋆}$ . Run Option II SCAFFOLD with a uniform size- $S$ client sample, $1 \leq S \leq N$ , and conditionally unbiased local stochastic gradients of variance at most $σ^{2}$ . Assume the client controls are updated to averages of the $K$ local stochastic gradients when selected, and define the control lag $C_{r}$ and local drift $E_{r}$ as in the SCAFFOLD analysis-trajectory definition. Then, for every $r \geq 1$ , $C_{r} \leq (1 - \frac{S}{N}) C_{r - 1} + \frac{S}{N} (4 β E [f (x_{r - 1}) - f^{⋆}] + 2 β^{2} E_{r}) .$

Statement references

Karimireddy et al., SCAFFOLD, Appendix E.1, Lemma 11 and its proof

Facts & Assumptions

Given: The Option II control updates, local paths and convex equal-client objective in the Statement.

[F1]

SCAFFOLD with client and server control variates: a selected client replaces its control by the average of the local gradients used in the round; an unselected control persists.

[F2]

SCAFFOLD trajectories, client drift, control lag and tracking error: $C_{r}$ is the expected squared error of the mean full gradient at a client's stored query anchors from $\nabla f_{i} (x^{⋆})$ , averaged over clients, and $E_{r}$ averages the squared displacements at the current gradient-query points $y_{i, k - 1}^{r}$ .

[F3]

Smooth convex gradient differences around a minimizer and Gradient of a finite sum is the finite sum of gradients: the average client gradient at the minimizer is zero and the population mean of squared client-gradient differences from $x^{⋆}$ is at most $2 β (f (x) - f^{⋆})$ .

[F4]

Relaxed inequalities for squared Euclidean norms and The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ : squared norms are convex and satisfy $∥ u + v ∥_{2}^{2} \leq 2 ∥ u ∥_{2}^{2} + 2 ∥ v ∥_{2}^{2}$ .

[F5]

Expectation of a nonnegative or integrable random variable and Linearity, monotonicity, and the modulus bound for expectation: expectations preserve the nonnegative inequalities and finite weighted averages used below.

Proof

1.1F1F2F5givenalgebra

Set $p = S / N$ . By [F1], a uniform sample retains a client's old query [given] anchors with probability $1 - p$ and replaces them with the current local query points with probability $p$ . The definition of $C_{r}$ in [F2] and Jensen's inequality for the average of $K$ vectors therefore give $C_{r} \leq (1 - p) C_{r - 1} + \frac{p}{N K} \sum_{i = 1}^{N} \sum_{k = 1}^{K} E ∥ \nabla f_{i} (y_{i, k - 1}^{r}) - \nabla f_{i} (x^{⋆}) ∥_{2}^{2} .$

2.1F2F3F4step 1.1givenalgebra∎

For each summand, decompose $\nabla f_{i} (y) - \nabla f_{i} (x^{⋆}) = (\nabla f_{i} (x_{r - 1}) - \nabla f_{i} (x^{⋆})) + (\nabla f_{i} (y) - \nabla f_{i} (x_{r - 1}))$ . By [F4], its squared norm is at most twice the squared norm of each term. Averaging the first term over clients and using [F3] gives at most $4 β E [f (x_{r - 1}) - f^{⋆}]$ ; averaging the second over clients and local steps and using $β$ -Lipschitzness gives at most $2 β^{2} E_{r}$ . Average step 1.1 over clients and substitute these two bounds to obtain the recurrence.

Depends on

Used by

Strongly convex SCAFFOLD progress in one communication round Lemma

Dependency tree · two levels

40 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 E.1, Lemma 11 (standard reference, not scraped)