Lemma 15 consequence — Convex and strongly convex convergence

Proved

SCAFFOLD.ConvexFiniteRoundConvergence

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

federated-learningprobabilitystochastic-optimization

Let $h\le1/(81\beta)$ and $\mu h\le S/(15N)$ . Set $q=1-\mu h/2$ , $w_r=q^{-(r+1)}$ for $0\le r<T$ , and $W_T=\sum_{r=0}^{T-1}w_r$ . Then $q\ge29/30>0$ and

\frac1{W_T}\sum_{r=0}^{T-1}w_r\,\mathbb E[f(x^r)-f(x^\star)] \le\frac{V_0}{hW_T}+\frac{12h\sigma^2}{KS}\left(1+\frac S{\eta_g^2}\right).

The case $\mu=0$ has uniform weights and $W_T=T$ ; $\mu>0$ gives geometric weights. No division by $\mu$ is used, and zero noise or zero initial distance is allowed.

Formalization note: a paper-derived finite-round formulation, obtained by weighted telescoping of Lemma 15, specialized to deterministic initial controls. It keeps all constants and the initial-control term, rather than transcribing the ambiguous asymptotic summary in Theorem VII. The statement itself does not assume Lemma 15 or any control-lag recurrence.

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.1, PDF p. 30, Lemma 15; PDF p. 31, first unnumbered averaging display; source-backed 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 ConvexFiniteRoundConvergence :
  ∀ (d N : ℕ) (P : Problem d N) (Ω : Type u) [MeasurableSpace Ω]
    [StandardBorelSpace Ω] (ν : Measure Ω) [IsProbabilityMeasure ν]
    (S K T : ℕ) (ηl ηg μ : ℝ) (c0 : Fin N → Space d) (xstar : Space d),
    Convexity P μ → IsMinimizer P xstar → 0 < ηl → 1 ≤ ηg →
    effectiveStep K ηl ηg ≤ 1 / (81 * P.β) →
    μ * effectiveStep K ηl ηg ≤ (S : ℝ) / (15 * (N : ℝ)) →
    ∀ A : Run P ν S K T ηl ηg (some c0),
      weightedGap A xstar μ ≤ convexRHS P S K T ηl ηg μ c0 xstar := 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.1, PDF p. 30, Lemma 15; PDF p. 31, first unnumbered averaging display; source-backed parent Section 5, PDF p. 5, Theorem III.

Read-back

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

Auditor model: gpt-6.

For every pair of natural numbers $d,N$ , let $V=\mathbb R^d$ with its Euclidean inner product and norm, and let the client indices be $i\in\{0,\ldots,N-1\}$ . Consider any collection of functions $f_i:V\to\mathbb R$ , constants $\beta,\sigma\in\mathbb R$ , and point $x_0\in V$ satisfying $N>0$ , $\beta>0$ , $\sigma\ge0$ , existence of the gradient $\nabla f_i(x)$ at every $x\in V$ for every client, and $\|\nabla f_i(x)-\nabla f_i(y)\|\le\beta\|x-y\|$ for every client and every $x,y\in V$ . Set $F(x)=N^{-1}\sum_{i=0}^{N-1}f_i(x)$ . For every standard Borel measurable space $\Omega$ (of any universe size), every probability measure $\nu$ on it, every $S,K,T\in\mathbb N$ , every $\eta_l,\eta_g,\mu\in\mathbb R$ , every deterministic collection $c_i^0\in V$ , and every $x_\star\in V$ , suppose $\mu\ge0$ and, for every client and all $x,y\in V$ ,

f_i(x)+\langle\nabla f_i(x),y-x\rangle+\frac{\mu}{2}\|y-x\|^2\le f_i(y),

suppose $F(x_\star)\le F(x)$ for every $x\in V$ , and suppose, writing $h=K\eta_l\eta_g$ ,

\eta_l>0,\qquad \eta_g\ge1,\qquad h\le\frac1{81\beta},\qquad \mu h\le\frac{S}{15N}.

The assertion applies to every run with the following data and properties. It requires $0<S\le N$ , $K>0$ , and $T>0$ . Its data consist of an increasing filtration $(\mathcal F_t)_{t\in\mathbb N}$ of sub- $\sigma$ -algebras of the measurable structure on $\Omega$ ; vector-valued maps $W_{k,i},X_r,C_{r,i},Y_{r,k,i},G_{r,k,i}:\Omega\to V$ for all natural time indices and all clients; and maps $I_r:\Omega\to\mathcal P(\{0,\ldots,N-1\})$ for all $r\in\mathbb N$ . Write $\tau_r=K+r(K+1)$ , write $\mathbb E_\nu[\cdot\mid\mathcal F_t]$ for conditional expectation with respect to $\nu$ , and interpret each equality or inequality of random variables below as holding $\nu$ -almost surely. For every $k<K$ and every client, $W_{k,i}$ is strongly $\mathcal F_{k+1}$ -measurable and belongs to $L^2(\nu;V)$ , and

\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.

For every $k<K$ , the family $(W_{k,i})_{i=0}^{N-1}$ is conditionally 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;V)$ . For every $r<T$ , every $k\le K$ , and every client, $Y_{r,k,i}$ is strongly $\mathcal F_{\tau_r+k}$ -measurable and belongs to $L^2(\nu;V)$ . For every $r<T$ , every $k<K$ , and every client, $G_{r,k,i}$ is strongly $\mathcal F_{\tau_r+k+1}$ -measurable and belongs to $L^2(\nu;V)$ , and

\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.

For every $r<T$ and every $k<K$ , the family $(G_{r,k,i})_{i=0}^{N-1}$ is conditionally independent given $\mathcal F_{\tau_r+k}$ . Here membership in $L^2(\nu;V)$ means almost-everywhere strong measurability and finite integral of the squared norm; the stated conditional independence is across clients at each fixed indicated time. For every $r<T$ , $|I_r|=S$ almost surely. For every $r<T$ and every subset $B\subseteq\{0,\ldots,N-1\}$ , the indicator $\mathbf1_{\{I_r=B\}}$ is strongly $\mathcal F_{\tau_{r+1}}$ -measurable and satisfies

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

The initialization is $X_0=x_0$ and $C_{0,i}=c_i^0$ for every client. For every $r<T$ and every client, $Y_{r,0,i}=X_r$ ; for every such $r,i$ and every $k<K$ ,

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

For every $r<T$ and every client,

C_{r+1,i}=\begin{cases}\displaystyle\frac1K\sum_{k=0}^{K-1}G_{r,k,i},&i\in I_r,\\C_{r,i},&i\notin I_r,\end{cases} \qquad X_{r+1}=X_r+\frac{\eta_g}{S}\sum_{i\in I_r}(Y_{r,K,i}-X_r).

All these initialization and update identities are almost-sure identities; their displayed random variables are evaluated at the same sample point. Define the real weights and their sum by

w_r=\left(\frac1{1-\mu h/2}\right)^{r+1},\qquad W=\sum_{r=0}^{T-1}w_r.

Then every such run satisfies

\frac1W\sum_{r=0}^{T-1}w_r\int_\Omega\bigl(F(X_r(\omega))-F(x_\star)\bigr)\,d\nu(\omega) \le \frac{\displaystyle\|x_0-x_\star\|^2+\frac{9Nh^2}{S}\left(\frac1N\sum_{i=0}^{N-1}\|c_i^0-\nabla f_i(x_\star)\|^2\right)}{hW} +\frac{12h\sigma^2}{KS}\left(1+\frac S{\eta_g^2}\right).

All natural numbers appearing in real-valued formulas are interpreted as real numbers. The averaged objective gaps concern rounds $0,\ldots,T-1$ , including the initial point and excluding $X_T$ . There is no requirement that $x_\star$ be the unique minimizer and no restriction on the deterministic initial controls beyond being vectors in $V$ . The warm variables still have to satisfy all the stated conditions although the supplied controls, rather than their averages, initialize this run. The maps are defined for all natural indices, but the displayed regularity, sampling, and update requirements apply only in their specified ranges. Dimension $d=0$ is included, giving the one-element zero-dimensional vector space. No problem data exist with $N=0$ ; for $S=0$ , $S>N$ , $K=0$ , or $T=0$ , no run of the required kind exists, so the universal assertion over runs is vacuous. In any existing run, $h>0$ , $\mu h\le1/15$ , $1-\mu h/2\ge29/30$ , and $W>0$ , so all displayed denominators are nonzero. The case $\mu=0$ is included and gives $w_r=1$ and $W=T$ ; zero noise $\sigma=0$ and full participation $S=N$ are also included. The theorem asserts this bound for every run satisfying its requirements and does not assert that such a run exists.

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