Lemma 19 consequence — Nonconvex convergence with warm start

Proved

SCAFFOLD.NonconvexFiniteRoundConvergence

by Minghui · Sep 23, 2026 · Mathlib c5ea003 (Lean v4.30.0)

federated-learningprobabilitystochastic-optimization

For the full-client $K$ -sample warm start, put $F=f(x^0)-f_{\rm low}$ and suppose $h\le(S/N)^{2/3}/(24\beta)$ . Then

\frac1T\sum_{r=0}^{T-1}\mathbb E\|\nabla f(x^r)\|^2 \le\frac{14F}{hT}+\frac{70\beta h\sigma^2}{KS}\left(1+\frac S{\eta_g^2}\right).

This includes $S=N$ , $K=1$ , $\sigma=0$ , and $F=0$ under the specified initialization.

Formalization note: a paper-derived finite-round formulation by summing Lemma 19, using the stated warm start to make the initial stored-point lag zero. The lower bound $f_{\rm low}$ makes explicit that attainment is unnecessary. No intermediate descent or control-lag estimate is assumed in the model. The factor $\beta$ and the sampling factor $1+S/\eta_g^2$ are retained from Lemma 19.

Source: Sai Praneeth Karimireddy, Satyen Kale, Mehryar Mohri, Sashank J. Reddi, Sebastian U. Stich, and Ananda Theertha Suresh, SCAFFOLD: Stochastic Controlled Averaging for Federated Learning, ICML 2020; arXiv:1910.06378v4, https://arxiv.org/abs/1910.06378v4; Appendix E.2, PDF p. 34, Lemma 19; PDF p. 35, final paragraph; PDF p. 31, equations (26)–(27); parent Section 5, PDF p. 5, Theorem III.

Notation and probability model

There are $N\ge1$ clients, a model space $\mathbb R^d$ (including $d=0$ ), differentiable client losses $f_i$ with $\beta$ -Lipschitz gradients, $\beta>0$ , and $f=N^{-1}\sum_i f_i$ . The starting point $x^0$ is deterministic and $\sigma\ge0$ bounds within-client stochastic-gradient standard deviation. A run has $T\ge1$ rounds, $K\ge1$ local steps, $1\le S\le N$ clients per round, local step $\eta_l>0$ , global step $\eta_g\ge1$ , and $h=K\eta_l\eta_g$ . All random variables live on a standard Borel probability space $(\Omega,\mathcal A,\nu)$ with a filtration containing the full history. States and gradient samples are square integrable; gradient samples are conditionally unbiased, have conditional squared error at most $\sigma^2$ , and are independent across clients conditional on each step's history. These are explicit fresh-oracle and finite-moment conventions.

Every round first defines virtual paths for all clients, starting at $y_{i,0}^r=x^r$ :

y_{i,k+1}^r=y_{i,k}^r-\eta_l(g_{i,k}^r-c_i^r+c^r),\qquad c^r=N^{-1}\sum_i c_i^r.

Then an $S$ -element subset is sampled uniformly, conditionally independently of these paths given the past. Equivalently, its conditional distribution given the entire completed virtual-path history is uniform. Only selected clients update their controls to $K^{-1}\sum_{k=0}^{K-1}g_{i,k}^r$ ; other controls persist. The server update is $x^{r+1}=x^r+(\eta_g/S)\sum_{i\in\mathcal S_r}(y_{i,K}^r-x^r)$ . This is option II of Algorithm 1, with the average-gradient form of Appendix E. The model contains the algorithm and oracle laws, not any convergence inequality.

For convex targets, $x^\star$ minimizes $f$ , and the client losses obey

f_i(y)\ge f_i(x)+\langle\nabla f_i(x),y-x\rangle +\frac\mu2\|y-x\|^2,\qquad \mu\ge0.

The initial client controls $c_i^0$ are arbitrary deterministic vectors and the server control is their average. Define

C_0=\frac1N\sum_i\|c_i^0-\nabla f_i(x^\star)\|^2,\qquad V_0=\|x^0-x^\star\|^2+\frac{9Nh^2}{S}C_0.

For nonconvex targets, $f_{\rm low}\le f(x)$ for all $x$ ; a minimizer need not exist. Each $c_i^0$ is instead initialized by averaging $K$ fresh stochastic gradients at $x^0$ , with the same conditional oracle assumptions. These full-client initialization queries are additional to the $T$ optimization rounds.

The output is a sampled pre-round server iterate among $x^0,\ldots,x^{T-1}$ , represented by its expected loss or squared-gradient statistic. No last-iterate or pathwise guarantee is asserted. Sources: Section 2, PDF p. 2; Algorithm 1, PDF p. 4; Appendix B.1, PDF p. 14, assumptions A3–A5; Appendix E, PDF pp. 25–26, equations (18)–(22), Remark 10; Appendix E.2, PDF pp. 31 and 35, equations (26)–(27) and final warm-start paragraph. Primary reference: Karimireddy et al., SCAFFOLD: Stochastic Controlled Averaging for Federated Learning, ICML 2020, https://arxiv.org/abs/1910.06378v4.

Preamble

import Definitions.Def_SCAFFOLD_Model
open MeasureTheory
universe u

Formal statement

namespace SCAFFOLD
theorem NonconvexFiniteRoundConvergence :
  ∀ (d N : ℕ) (P : Problem d N) (Ω : Type u) [MeasurableSpace Ω]
    [StandardBorelSpace Ω] (ν : Measure Ω) [IsProbabilityMeasure ν]
    (S K T : ℕ) (ηl ηg fLower : ℝ),
    (∀ x, fLower ≤ objective P.f x) → 0 < ηl → 1 ≤ ηg →
    effectiveStep K ηl ηg ≤
      Real.rpow ((S : ℝ) / (N : ℝ)) (2 / 3 : ℝ) / (24 * P.β) →
    ∀ A : Run P ν S K T ηl ηg none,
      averageGradientSq A ≤ nonconvexRHS P S K T ηl ηg fLower := by sorry
end SCAFFOLD

Source

Sai Praneeth Karimireddy, Satyen Kale, Mehryar Mohri, Sashank J. Reddi, Sebastian U. Stich, and Ananda Theertha Suresh, SCAFFOLD: Stochastic Controlled Averaging for Federated Learning, ICML 2020; arXiv:1910.06378v4, https://arxiv.org/abs/1910.06378v4; Appendix E.2, PDF p. 34, Lemma 19; PDF p. 35, final paragraph; PDF p. 31, equations (26)–(27); parent Section 5, PDF p. 5, Theorem III.

Read-back

What the Lean code literally says, in plain math · gpt-6

NonconvexFiniteRoundConvergence

Read-back model: gpt-6.

For every pair of natural numbers $d,N$ , let $E=\mathbb R^{\{0,\ldots,d-1\}}$ with its Euclidean inner product and norm, and let $I=\{0,\ldots,N-1\}$ . Let $P$ consist of a positive client count $N>0$ , functions $f_i:E\to\mathbb R$ for $i\in I$ , real numbers $\beta>0$ and $\sigma\ge0$ , and a point $x_0\in E$ , with the following properties: each $f_i$ has a gradient at every $z\in E$ , equal to the gradient appearing below, and $\|\nabla f_i(z)-\nabla f_i(w)\|\le\beta\|z-w\|$ for every $i,z,w$ . Define $F(z)=N^{-1}\sum_{i\in I}f_i(z)$ . For every type $\Omega$ in an arbitrary universe, equipped with a measurable space that is standard Borel, every probability measure $\nu$ on that space, every $S,K,T\in\mathbb N$ , and every $\eta_l,\eta_g,f_{\mathrm{low}}\in\mathbb R$ , suppose $f_{\mathrm{low}}\le F(z)$ for every $z\in E$ , $\eta_l>0$ , $\eta_g\ge1$ , and, writing $h=K\eta_l\eta_g$ , suppose

h\le\frac{(S/N)^{2/3}}{24\beta},

where the exponent denotes the real power. The assertion holds for every collection $A$ of the following data and properties (all equalities and inequalities between random quantities below are $\nu$ -almost sure unless otherwise specified). The collection requires $0<S\le N$ , $0<K$ , and $0<T$ ; an increasing sequence $(\mathcal F_t)_{t\in\mathbb N}$ of sub- $\sigma$ -algebras of the given measurable space; random vectors $W_{k,i}$ for every $k\in\mathbb N,i\in I$ , $X_r$ and $C_{r,i}$ for every $r\in\mathbb N,i\in I$ , $Y_{r,k,i}$ and $G_{r,k,i}$ for every $r,k\in\mathbb N,i\in I$ ; and a finite-subset-valued function $B_r:\Omega\to\mathcal P(I)$ for every $r\in\mathbb N$ . Set $\tau_r=K+r(K+1)$ . For every $k<K$ and every $i\in I$ , $W_{k,i}$ is strongly $\mathcal F_{k+1}$ -measurable and belongs to $L^2(\nu;E)$ (that is, it is almost everywhere strongly measurable with finite second moment),

\mathbb E_\nu[W_{k,i}\mid\mathcal F_k]=\nabla f_i(x_0),\qquad \mathbb E_\nu[\|W_{k,i}-\nabla f_i(x_0)\|^2\mid\mathcal F_k]\le\sigma^2,

and, for each such $k$ , the full family $(W_{k,i})_{i\in I}$ is conditionally mutually independent given $\mathcal F_k$ . For every $r\le T$ , $X_r$ and each $C_{r,i}$ are strongly $\mathcal F_{\tau_r}$ -measurable and belong to $L^2(\nu;E)$ . For every $r<T$ , $k\le K$ , and $i\in I$ , $Y_{r,k,i}$ is strongly $\mathcal F_{\tau_r+k}$ -measurable and belongs to $L^2(\nu;E)$ . For every $r<T$ , $k<K$ , and $i\in I$ , $G_{r,k,i}$ is strongly $\mathcal F_{\tau_r+k+1}$ -measurable and belongs to $L^2(\nu;E)$ ,

\mathbb E_\nu[G_{r,k,i}\mid\mathcal F_{\tau_r+k}] =\nabla f_i(Y_{r,k,i}),\qquad \mathbb E_\nu[\|G_{r,k,i}-\nabla f_i(Y_{r,k,i})\|^2\mid\mathcal F_{\tau_r+k}]\le\sigma^2,

and, for every such $r,k$ , the full family $(G_{r,k,i})_{i\in I}$ is conditionally mutually independent given $\mathcal F_{\tau_r+k}$ . For every $r<T$ , $|B_r|=S$ almost surely; for every finite subset $D\subseteq I$ , the real indicator $\mathbf1_{\{B_r=D\}}$ is strongly $\mathcal F_{\tau_{r+1}}$ -measurable and satisfies

\mathbb E_\nu[\mathbf1_{\{B_r=D\}}\mid\mathcal F_{\tau_r+K}] = \begin{cases} \binom{N}{S}^{-1},& |D|=S,\\ 0,& |D|\ne S. \end{cases}

The required initialization is $X_0=x_0$ and, for each $i\in I$ , $C_{0,i}=K^{-1}\sum_{k=0}^{K-1}W_{k,i}$ . For every $r<T$ and $i\in I$ , $Y_{r,0,i}=X_r$ ; for every additional $k<K$ , the local update is

Y_{r,k+1,i} =Y_{r,k,i}-\eta_l\left(G_{r,k,i}-C_{r,i}+\frac1N\sum_{j\in I}C_{r,j}\right).

For every $r<T$ and $i\in I$ , the control update, evaluated at each outcome, is

C_{r+1,i} =\begin{cases} \displaystyle\frac1K\sum_{k=0}^{K-1}G_{r,k,i},& i\in B_r,\\ C_{r,i},&i\notin B_r, \end{cases}

and the server update for each $r<T$ is

X_{r+1}=X_r+\frac{\eta_g}{S}\sum_{i\in B_r}(Y_{r,K,i}-X_r).

Under precisely these hypotheses, the conclusion is

\frac1T\sum_{r=0}^{T-1}\int_\Omega\|\nabla F(X_r(\omega))\|^2\,d\nu(\omega) \le \frac{14\bigl(F(x_0)-f_{\mathrm{low}}\bigr)}{hT} +\frac{70\beta h\sigma^2}{KS}\left(1+\frac{S}{\eta_g^2}\right).

Here every natural number used in real arithmetic is understood as its real-valued image; the expectations are conditional expectations under $\nu$ , and the integrals are measure-theoretic integrals under $\nu$ . No convexity, minimizer, attainment of $f_{\mathrm{low}}$ , or existence of such a collection $A$ is asserted or assumed separately. The arrays are defined at all natural indices, but only the index ranges explicitly stated above are constrained. The measurability, moment, gradient, and update conditions cover all clients, including clients outside $B_r$ . The conclusion averages the iterates with indices $0,\ldots,T-1$ , excluding $X_T$ . The universal quantifiers include $d=0$ , where $E$ is the zero-dimensional Euclidean space, every vector and gradient is zero, and the left side is zero; they permit $N=S=K=T=1$ and $\sigma=0$ . An instance of $P$ excludes $N=0$ , and an instance of $A$ excludes $S=0$ , $K=0$ , $T=0$ , and $S>N$ ; if these parameters preclude such an instance, the corresponding assertion over all $A$ has no instances. An empty $\Omega$ cannot carry the assumed probability measure. The subset condition also quantifies over $D=\varnothing$ , giving conditional probability zero since $S>0$ . For an actual instance all of $N,S,K,T,\beta,\eta_g,h$ are strictly positive, as is $\binom{N}{S}$ , so none of the displayed denominators vanishes and the sums over clients, local steps, rounds, and sampled clients are nonempty. The lower-bound assumption also gives $F(x_0)-f_{\mathrm{low}}\ge0$ .

Human review

Endorsed by Shuze Chen · Sep 24, 2026
Confirmed by the moderator at approval.
Endorsed by Minghui · Sep 24, 2026
Confirmed by the mission captain (proposal self-audit).

View graph