Prove2Me
Navigate
DiscoverFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

SCAFFOLD convergence — Explicit finite-round forms supporting Theorem III

Proved
SCAFFOLD.FiniteRoundConvergence

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

federated-learningprobabilitystochastic-optimization

The goal is the conjunction of the following two uniformly quantified finite-round guarantees.

Let h≤1/(81β)h\le1/(81\beta)h≤1/(81β) and μh≤S/(15N)\mu h\le S/(15N)μh≤S/(15N). Set q=1−μh/2q=1-\mu h/2q=1−μh/2, wr=q−(r+1)w_r=q^{-(r+1)}wr​=q−(r+1) for 0≤r<T0\le r<T0≤r<T, and WT=∑r=0T−1wrW_T=\sum_{r=0}^{T-1}w_rWT​=∑r=0T−1​wr​. Then q≥29/30>0q\ge29/30>0q≥29/30>0 and

1WT∑r=0T−1wr E[f(xr)−f(x⋆)]≤V0hWT+12hσ2KS(1+Sηg2).\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).WT​1​r=0∑T−1​wr​E[f(xr)−f(x⋆)]≤hWT​V0​​+KS12hσ2​(1+ηg2​S​).

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

For the full-client KKK-sample warm start, put F=f(x0)−flowF=f(x^0)-f_{\rm low}F=f(x0)−flow​ and suppose h≤(S/N)2/3/(24β)h\le(S/N)^{2/3}/(24\beta)h≤(S/N)2/3/(24β). Then

1T∑r=0T−1E∥∇f(xr)∥2≤14FhT+70βhσ2KS(1+Sηg2).\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).T1​r=0∑T−1​E∥∇f(xr)∥2≤hT14F​+KS70βhσ2​(1+ηg2​S​).

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

Formalization note: this is an explicit, paper-derived formulation of the finite-round convergence guarantees underlying Theorem III, not a literal formalization of its big-OOO notation or a claim about last iterates. Rate optimization and initialization communication accounting are further corollaries, not extra hypotheses. The two branches use their stated, different initializations. The source audit documents the appendix sign, drift-index, control-expectation, and asymptotic-summary issues; none of those ambiguous expressions is used as a model assumption.

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; Section 5, PDF p. 5, Theorem III; Appendix E, PDF p. 25, Theorem VII; Appendix E.1, PDF p. 30, Lemma 15 and PDF p. 31 averaging display; Appendix E.2, PDF p. 34, Lemma 19 and PDF p. 35 final paragraph.

Notation and probability model

There are N≥1N\ge1N≥1 clients, a model space Rd\mathbb R^dRd (including d=0d=0d=0), differentiable client losses fif_ifi​ with β\betaβ-Lipschitz gradients, β>0\beta>0β>0, and f=N−1∑ifif=N^{-1}\sum_i f_if=N−1∑i​fi​. The starting point x0x^0x0 is deterministic and σ≥0\sigma\ge0σ≥0 bounds within-client stochastic-gradient standard deviation. A run has T≥1T\ge1T≥1 rounds, K≥1K\ge1K≥1 local steps, 1≤S≤N1\le S\le N1≤S≤N clients per round, local step ηl>0\eta_l>0ηl​>0, global step ηg≥1\eta_g\ge1ηg​≥1, and h=Kηlηgh=K\eta_l\eta_gh=Kηl​ηg​. All random variables live on a standard Borel probability space (Ω,A,ν)(\Omega,\mathcal A,\nu)(Ω,A,ν) 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 σ2\sigma^2σ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 yi,0r=xry_{i,0}^r=x^ryi,0r​=xr:

yi,k+1r=yi,kr−ηl(gi,kr−cir+cr),cr=N−1∑icir.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.yi,k+1r​=yi,kr​−ηl​(gi,kr​−cir​+cr),cr=N−1i∑​cir​.

Then an SSS-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∑k=0K−1gi,krK^{-1}\sum_{k=0}^{K-1}g_{i,k}^rK−1∑k=0K−1​gi,kr​; other controls persist. The server update is xr+1=xr+(ηg/S)∑i∈Sr(yi,Kr−xr)x^{r+1}=x^r+(\eta_g/S)\sum_{i\in\mathcal S_r}(y_{i,K}^r-x^r)xr+1=xr+(ηg​/S)∑i∈Sr​​(yi,Kr​−xr). 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⋆x^\starx⋆ minimizes fff, and the client losses obey

fi(y)≥fi(x)+⟨∇fi(x),y−x⟩+μ2∥y−x∥2,μ≥0.f_i(y)\ge f_i(x)+\langle\nabla f_i(x),y-x\rangle +\frac\mu2\|y-x\|^2,\qquad \mu\ge0.fi​(y)≥fi​(x)+⟨∇fi​(x),y−x⟩+2μ​∥y−x∥2,μ≥0.

The initial client controls ci0c_i^0ci0​ are arbitrary deterministic vectors and the server control is their average. Define

C0=1N∑i∥ci0−∇fi(x⋆)∥2,V0=∥x0−x⋆∥2+9Nh2SC0.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.C0​=N1​i∑​∥ci0​−∇fi​(x⋆)∥2,V0​=∥x0−x⋆∥2+S9Nh2​C0​.

For nonconvex targets, flow≤f(x)f_{\rm low}\le f(x)flow​≤f(x) for all xxx; a minimizer need not exist. Each ci0c_i^0ci0​ is instead initialized by averaging KKK fresh stochastic gradients at x0x^0x0, with the same conditional oracle assumptions. These full-client initialization queries are additional to the TTT optimization rounds.

The output is a sampled pre-round server iterate among x0,…,xT−1x^0,\ldots,x^{T-1}x0,…,xT−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 FiniteRoundConvergence :
(
  ∀ (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
) ∧ (
  ∀ (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; Section 5, PDF p. 5, Theorem III; Appendix E, PDF p. 25, Theorem VII; Appendix E.1, PDF p. 30, Lemma 15 and PDF p. 31 averaging display; Appendix E.2, PDF p. 34, Lemma 19 and PDF p. 35 final paragraph.
Read-back

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

Read-back model: gpt-6.

The declaration asserts a conjunction of two independently universally quantified bounds, with the following common data and run requirements. For an arbitrary universe level, each bound quantifies over natural numbers d,Nd,Nd,N, a problem PPP, a type Ω\OmegaΩ in that universe equipped with a measurable space that is a standard Borel space, a probability measure ν\nuν on Ω\OmegaΩ, natural numbers S,K,TS,K,TS,K,T, and real numbers ηl,ηg\eta_l,\eta_gηl​,ηg​. Write I={0,…,N−1}I=\{0,\ldots,N-1\}I={0,…,N−1} and E=RdE=\mathbb R^dE=Rd, with its Euclidean norm and real inner product. The problem PPP consists of functions fi:E→Rf_i:E\to\mathbb Rfi​:E→R for i∈Ii\in Ii∈I, real numbers β,σ\beta,\sigmaβ,σ, and x0∈Ex_0\in Ex0​∈E, subject to N>0N>0N>0, β>0\beta>0β>0, σ≥0\sigma\ge0σ≥0, existence of the gradient ∇fi(x)\nabla f_i(x)∇fi​(x) at every i,xi,xi,x, and

∥∇fi(x)−∇fi(y)∥≤β∥x−y∥(i∈I, x,y∈E).\|\nabla f_i(x)-\nabla f_i(y)\|\le\beta\|x-y\| \qquad(i\in I,\ x,y\in E).∥∇fi​(x)−∇fi​(y)∥≤β∥x−y∥(i∈I, x,y∈E).

Define the real-valued objective, round times, and effective step by

F(x)=1N∑i∈Ifi(x),tr=K+r(K+1)(r∈N),h=Kηlηg.F(x)=\frac1N\sum_{i\in I}f_i(x),\qquad t_r=K+r(K+1)\quad(r\in\mathbb N),\qquad h=K\eta_l\eta_g.F(x)=N1​i∈I∑​fi​(x),tr​=K+r(K+1)(r∈N),h=Kηl​ηg​.

Natural numbers occurring in real formulas are interpreted as real numbers.

A run at these parameters requires 0<S≤N0<S\le N0<S≤N, K>0K>0K>0, and T>0T>0T>0. It supplies a filtration (Ft)t∈N(\mathscr F_t)_{t\in\mathbb N}(Ft​)t∈N​ of sub-σ\sigmaσ-algebras of the specified measurable space on Ω\OmegaΩ; random vectors

Uk,i,Xr,Cr,i,Yr,k,i,Gr,k,i:Ω→E(r,k∈N, i∈I);U_{k,i},X_r,C_{r,i},Y_{r,k,i},G_{r,k,i}:\Omega\to E \qquad(r,k\in\mathbb N,\ i\in I);Uk,i​,Xr​,Cr,i​,Yr,k,i​,Gr,k,i​:Ω→E(r,k∈N, i∈I);

and maps Br:Ω→{finite subsets of I}B_r:\Omega\to\{\text{finite subsets of }I\}Br​:Ω→{finite subsets of I} for all r∈Nr\in\mathbb Nr∈N. All almost-sure statements below are with respect to ν\nuν, and Eν[ ⋅∣Ft]\mathbb E_\nu[\,\cdot\mid\mathscr F_t]Eν​[⋅∣Ft​] denotes conditional expectation. The warm-up vectors satisfy, for every k<Kk<Kk<K and i∈Ii\in Ii∈I, strong measurability of Uk,iU_{k,i}Uk,i​ with respect to Fk+1\mathscr F_{k+1}Fk+1​, membership Uk,i∈L2(ν;E)U_{k,i}\in L^2(\nu;E)Uk,i​∈L2(ν;E), and

Eν[Uk,i∣Fk]=∇fi(x0)almost surely,Eν[∥Uk,i−∇fi(x0)∥2∣Fk]≤σ2almost surely.\mathbb E_\nu[U_{k,i}\mid\mathscr F_k] =\nabla f_i(x_0)\quad\text{almost surely},\qquad \mathbb E_\nu[\|U_{k,i}-\nabla f_i(x_0)\|^2\mid\mathscr F_k] \le\sigma^2\quad\text{almost surely}.Eν​[Uk,i​∣Fk​]=∇fi​(x0​)almost surely,Eν​[∥Uk,i​−∇fi​(x0​)∥2∣Fk​]≤σ2almost surely.

For each k<Kk<Kk<K, the whole family (Uk,i)i∈I(U_{k,i})_{i\in I}(Uk,i​)i∈I​ is conditionally independent given Fk\mathscr F_kFk​. For every r≤Tr\le Tr≤T, XrX_rXr​ and each Cr,iC_{r,i}Cr,i​ are strongly measurable with respect to Ftr\mathscr F_{t_r}Ftr​​ and belong to L2(ν;E)L^2(\nu;E)L2(ν;E). For every r<Tr<Tr<T, k≤Kk\le Kk≤K, and i∈Ii\in Ii∈I, Yr,k,iY_{r,k,i}Yr,k,i​ is strongly measurable with respect to Ftr+k\mathscr F_{t_r+k}Ftr​+k​ and belongs to L2(ν;E)L^2(\nu;E)L2(ν;E). For every r<Tr<Tr<T, k<Kk<Kk<K, and i∈Ii\in Ii∈I, Gr,k,iG_{r,k,i}Gr,k,i​ is strongly measurable with respect to Ftr+k+1\mathscr F_{t_r+k+1}Ftr​+k+1​, belongs to L2(ν;E)L^2(\nu;E)L2(ν;E), and satisfies

Eν[Gr,k,i∣Ftr+k]=∇fi(Yr,k,i)almost surely,Eν[∥Gr,k,i−∇fi(Yr,k,i)∥2∣Ftr+k]≤σ2almost surely.\begin{aligned} \mathbb E_\nu[G_{r,k,i}\mid\mathscr F_{t_r+k}] &=\nabla f_i(Y_{r,k,i}) &&\text{almost surely},\\ \mathbb E_\nu[\|G_{r,k,i}-\nabla f_i(Y_{r,k,i})\|^2 \mid\mathscr F_{t_r+k}] &\le\sigma^2 &&\text{almost surely}. \end{aligned}Eν​[Gr,k,i​∣Ftr​+k​]Eν​[∥Gr,k,i​−∇fi​(Yr,k,i​)∥2∣Ftr​+k​]​=∇fi​(Yr,k,i​)≤σ2​​almost surely,almost surely.​

Here a function applied to a random vector is evaluated pointwise on Ω\OmegaΩ. For each r<Tr<Tr<T and k<Kk<Kk<K, the whole family (Gr,k,i)i∈I(G_{r,k,i})_{i\in I}(Gr,k,i​)i∈I​ is conditionally independent given Ftr+k\mathscr F_{t_r+k}Ftr​+k​.

For each r<Tr<Tr<T, the sampled set has ∣Br∣=S|B_r|=S∣Br​∣=S almost surely. For every finite subset J⊆IJ\subseteq IJ⊆I, the real-valued indicator 1{Br=J}\mathbf1_{\{B_r=J\}}1{Br​=J}​ is strongly measurable with respect to Ftr+1\mathscr F_{t_{r+1}}Ftr+1​​, and

Eν[1{Br=J}∣Ftr+K]={(NS)−1,∣J∣=S,0,∣J∣≠Salmost surely.\mathbb E_\nu[\mathbf1_{\{B_r=J\}}\mid\mathscr F_{t_r+K}] = \begin{cases} \binom{N}{S}^{-1},& |J|=S,\\ 0,& |J|\ne S \end{cases} \quad\text{almost surely}.Eν​[1{Br​=J}​∣Ftr​+K​]={(SN​)−1,0,​∣J∣=S,∣J∣=S​almost surely.

The run has X0=x0X_0=x_0X0​=x0​ almost surely. Its initial controls are specified separately in the two bounds below. For every r<Tr<Tr<T and i∈Ii\in Ii∈I, it has Yr,0,i=XrY_{r,0,i}=X_rYr,0,i​=Xr​ almost surely. For every r<Tr<Tr<T, k<Kk<Kk<K, and i∈Ii\in Ii∈I, its local update is

Yr,k+1,i=Yr,k,i−ηl(Gr,k,i−Cr,i+1N∑j∈ICr,j)almost surely.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) \quad\text{almost surely}.Yr,k+1,i​=Yr,k,i​−ηl​​Gr,k,i​−Cr,i​+N1​j∈I∑​Cr,j​​almost surely.

For every r<Tr<Tr<T and i∈Ii\in Ii∈I, its control update is

Cr+1,i(ω)={1K∑k=0K−1Gr,k,i(ω),i∈Br(ω),Cr,i(ω),i∉Br(ω)for almost every ω.C_{r+1,i}(\omega)= \begin{cases} \displaystyle\frac1K\sum_{k=0}^{K-1}G_{r,k,i}(\omega), &i\in B_r(\omega),\\ C_{r,i}(\omega),&i\notin B_r(\omega) \end{cases} \quad\text{for almost every }\omega.Cr+1,i​(ω)=⎩⎨⎧​K1​k=0∑K−1​Gr,k,i​(ω),Cr,i​(ω),​i∈Br​(ω),i∈/Br​(ω)​for almost every ω.

For every r<Tr<Tr<T, its server update is

Xr+1(ω)=Xr(ω)+ηgS∑i∈Br(ω)(Yr,K,i(ω)−Xr(ω))for almost every ω.X_{r+1}(\omega)=X_r(\omega) +\frac{\eta_g}{S}\sum_{i\in B_r(\omega)} \bigl(Y_{r,K,i}(\omega)-X_r(\omega)\bigr) \quad\text{for almost every }\omega.Xr+1​(ω)=Xr​(ω)+Sηg​​i∈Br​(ω)∑​(Yr,K,i​(ω)−Xr​(ω))for almost every ω.

These requirements impose the local dynamics and gradient assumptions on every client i∈Ii\in Ii∈I, including clients outside Br(ω)B_r(\omega)Br​(ω). Each displayed almost-sure identity or inequality is required separately for the indicated indices. All of the warm-up requirements are part of a run in both bounds, including when its controls are initialized deterministically.

The first universally quantified bound additionally quantifies over a real number μ\muμ, an arbitrary deterministic function c0:I→Ec_0:I\to Ec0​:I→E, and x⋆∈Ex_\star\in Ex⋆​∈E. It assumes μ≥0\mu\ge0μ≥0 and, for every i∈Ii\in Ii∈I and every x,y∈Ex,y\in Ex,y∈E,

fi(x)+⟨∇fi(x),y−x⟩+μ2∥y−x∥2≤fi(y).f_i(x)+\langle\nabla f_i(x),y-x\rangle +\frac\mu2\|y-x\|^2\le f_i(y).fi​(x)+⟨∇fi​(x),y−x⟩+2μ​∥y−x∥2≤fi​(y).

It also assumes

F(x⋆)≤F(x)for every x∈E,ηl>0,ηg≥1,h≤181β,μh≤S15N.\begin{gathered} F(x_\star)\le F(x)\quad\text{for every }x\in E,\qquad \eta_l>0,\qquad \eta_g\ge1,\\ h\le\frac1{81\beta},\qquad \mu h\le\frac{S}{15N}. \end{gathered}F(x⋆​)≤F(x)for every x∈E,ηl​>0,ηg​≥1,h≤81β1​,μh≤15NS​.​

For every run satisfying all the common requirements and the deterministic control initialization C0,i=c0(i)C_{0,i}=c_0(i)C0,i​=c0​(i) almost surely for every i∈Ii\in Ii∈I, let

wr=(1−μh/2)−(r+1)(0≤r<T),W=∑r=0T−1wr.w_r=(1-\mu h/2)^{-(r+1)} \quad(0\le r<T),\qquad W=\sum_{r=0}^{T-1}w_r.wr​=(1−μh/2)−(r+1)(0≤r<T),W=r=0∑T−1​wr​.

The asserted bound is

1W∑r=0T−1wr∫Ω(F(Xr(ω))−F(x⋆)) dν(ω)≤∥x0−x⋆∥2+9Nh2S(1N∑i∈I∥c0(i)−∇fi(x⋆)∥2)hW+12hσ2KS(1+Sηg2).\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\in I}\|c_0(i)-\nabla f_i(x_\star)\|^2 \right)} {hW} +\frac{12h\sigma^2}{KS}\left(1+\frac{S}{\eta_g^2}\right).W1​r=0∑T−1​wr​∫Ω​(F(Xr​(ω))−F(x⋆​))dν(ω)≤hW∥x0​−x⋆​∥2+S9Nh2​(N1​i∈I∑​∥c0​(i)−∇fi​(x⋆​)∥2)​+KS12hσ2​(1+ηg2​S​).

The left side is the weighted sum of the expected objective gaps at X0,…,XT−1X_0,\ldots,X_{T-1}X0​,…,XT−1​, divided by the sum of those weights.

The second universally quantified bound independently quantifies over all the common data and a real number flowerf_{\mathrm{lower}}flower​. It assumes

flower≤F(x)for every x∈E,ηl>0,ηg≥1,h≤(S/N)2/324β,\begin{gathered} f_{\mathrm{lower}}\le F(x)\quad\text{for every }x\in E,\qquad \eta_l>0,\qquad \eta_g\ge1,\\ h\le\frac{(S/N)^{2/3}}{24\beta}, \end{gathered}flower​≤F(x)for every x∈E,ηl​>0,ηg​≥1,h≤24β(S/N)2/3​,​

where (S/N)2/3(S/N)^{2/3}(S/N)2/3 is the real power with exponent 2/32/32/3. For every run satisfying all the common requirements and the warm-up control initialization

C0,i=1K∑k=0K−1Uk,ialmost surely(i∈I),C_{0,i}=\frac1K\sum_{k=0}^{K-1}U_{k,i} \quad\text{almost surely}\qquad(i\in I),C0,i​=K1​k=0∑K−1​Uk,i​almost surely(i∈I),

the asserted bound is

1T∑r=0T−1∫Ω∥∇F(Xr(ω))∥2 dν(ω)≤14(F(x0)−flower)hT+70βhσ2KS(1+Sηg2).\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{lower}}\bigr)}{hT} +\frac{70\beta h\sigma^2}{KS} \left(1+\frac{S}{\eta_g^2}\right).T1​r=0∑T−1​∫Ω​∥∇F(Xr​(ω))∥2dν(ω)≤hT14(F(x0​)−flower​)​+KS70βhσ2​(1+ηg2​S​).

Here ∇F\nabla F∇F is the Euclidean gradient of the explicitly defined average FFF. This conjunct has no convexity or minimizer hypothesis. The conjunction asserts both universal implications; it does not require the data or the run in one conjunct to coincide with those in the other.

The quantifiers allow d=0d=0d=0, when EEE is the zero-dimensional Euclidean space with one point, and allow σ=0\sigma=0σ=0. They include N=1N=1N=1, S=1S=1S=1, K=1K=1K=1, T=1T=1T=1, and full participation S=NS=NS=N whenever the other hypotheses hold. For the first bound, μ=0\mu=0μ=0 is allowed and gives wr=1w_r=1wr​=1 and W=TW=TW=T. Although N,S,K,TN,S,K,TN,S,K,T are quantified as arbitrary natural numbers, N=0N=0N=0 admits no problem PPP, and S=0S=0S=0, S>NS>NS>N, K=0K=0K=0, or T=0T=0T=0 admits no run of the required kind. The universal assertion over runs is vacuous whenever no such run exists; neither conjunct asserts existence of a run. The first conjunct assumes the supplied x⋆x_\starx⋆​ is a minimizer, and the second assumes the supplied real flowerf_{\mathrm{lower}}flower​ is a global lower bound, without asserting existence of either. In an actual run meeting either conjunct's step assumptions, N,S,K,T,β,ηg,hN,S,K,T,\beta,\eta_g,hN,S,K,T,β,ηg​,h are all positive. In the first conjunct, 0≤μh≤S/(15N)≤1/150\le\mu h\le S/(15N)\le1/150≤μh≤S/(15N)≤1/15, hence 1−μh/2≥29/30>01-\mu h/2\ge29/30>01−μh/2≥29/30>0 and W>0W>0W>0. Thus the displayed denominators are nonzero in all instances with an admissible run. The run's arrays are defined for all natural time indices, but measurability, moment, independence, and update conditions apply only over the index ranges explicitly stated above; the bounds use X0,…,XT−1X_0,\ldots,X_{T-1}X0​,…,XT−1​, while the run also constrains XTX_TXT​ and CT,iC_{T,i}CT,i​. Conditional independence is imposed for each indicated family across clients at a fixed warm-up step or local step; it does not itself assert independence across different steps. All integrals are the measure-theoretic integrals from the declaration, with their total-function convention of value zero for a nonintegrable integrand; no separate integrability hypothesis for the two displayed objective-gap or squared-gradient integrands is included in the theorem statement.

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

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, with reuse governed by our licensing terms.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me