Theorem 1 — Convex FedAvg Convergence (constant step)

ConvexFedAvgConvergence specifies a proposition; this declaration supplies no proof of it. For every pair of natural numbers $d,M$, consider the Euclidean space $E=\mathbb R^d$ with its Euclidean norm and a problem consisting of $M>0$ functions $f_i:E\to\mathbb R$, indexed by $i\in\{0,\ldots,M-1\}$, real parameters $L>0$, $\sigma\ge0$, $\zeta\ge0$, and points $x_0,x_\star\in E$. Put $F(x)=M^{-1}\sum_{i=0}^{M-1}f_i(x)$. At every $x\in E$ each $f_i$ has its declared gradient $\nabla f_i(x)$, each $f_i$ is convex on all of $E$, and for all clients $i$ and all $x,y\in E$ one has $\|\nabla f_i(x)-\nabla f_i(y)\|\le L\|x-y\|$ and $\|\nabla f_i(x)-\nabla F(x)\|\le\zeta$. The point $x_\star$ satisfies $F(x_\star)\le F(x)$ for every $x\in E$. Universally quantify also over a type $\Omega$ in the declaration's arbitrary universe $u$, a measurable-space structure on $\Omega$ that makes it a standard Borel space, and a probability measure $\mu$ on that space. Write $\mathbb E_\mu$ for integration against $\mu$ and $\mathbb E_\mu[\,\cdot\mid\mathcal H_s]$ for the library's conditional expectation given $\mathcal H_s$. Universally quantify over natural numbers $\tau,T$ and a real number $\eta$ satisfying $\tau>0$, $T>0$, and $0<\eta\le1/(4L)$. For the specified $\tau,T,\eta$, a run consists of an increasing filtration $(\mathcal H_s)_{s\in\mathbb N}$ of sub-$\sigma$-algebras of the ambient measurable space and functions $x_{t,k,i},g_{t,k,i}:\Omega\to E$ defined for every $t,k\in\mathbb N$ and client $i$. For every $t<T$, $k\le\tau$, and $i$, $x_{t,k,i}$ is strongly $\mathcal H_{t\tau+k}$-measurable and square-integrable against $\mu$. For every $t<T$, $k<\tau$, and $i$, $g_{t,k,i}$ is strongly $\mathcal H_{t\tau+k+1}$-measurable and square-integrable, and the following hold $\mu$-almost everywhere: $\mathbb E_\mu[g_{t,k,i}\mid\mathcal H_{t\tau+k}]=\nabla f_i(x_{t,k,i})$, $\mathbb E_\mu[\|g_{t,k,i}-\nabla f_i(x_{t,k,i})\|^2\mid\mathcal H_{t\tau+k}]\le\sigma^2$, and $x_{t,k+1,i}=x_{t,k,i}-\eta g_{t,k,i}$. For each such $t,k$, the whole family $(g_{t,k,i})_{i=0}^{M-1}$ is mutually conditionally independent given $\mathcal H_{t\tau+k}$; explicitly, conditional probabilities of intersections of finitely many events $\{g_{t,k,i}\in A_i\}$ with distinct clients and Borel sets $A_i\subseteq E$ equal the products of their conditional probabilities almost everywhere. The initialization $x_{0,0,i}(\omega)=x_0$ holds for every client and every $\omega$, with no exceptional null set. For each $t$ with $t+1<T$ and each $i$, synchronization satisfies $x_{t+1,0,i}=M^{-1}\sum_jx_{t,\tau,j}$ almost everywhere. Define $\bar x_{t,k}=M^{-1}\sum_i x_{t,k,i}$. Write $D=\|x_0-x_\star\|$. The proposition states that every such run satisfies

The left side integrates an average of objective excesses at the averaged iterates with inner indices $1,\ldots,\tau$ in each round. Values $D=0$, $\sigma=0$, and $\zeta=0$ are allowed. The positivity hypotheses make the displayed explicit rational denominators nonzero. This proposition has no other proposition from the bundle as a premise. The dimension $d=0$ is permitted, as is $M=1$; $M=0$ is excluded by the problem data. No existence or uniqueness of a run is asserted. The run requirements impose no additional restrictions outside the specified index ranges, apart from the universally imposed initialization. Equalities and inequalities involving conditional expectations or updates are only almost-everywhere statements unless explicitly stated otherwise. Conditional expectation here is a selected function version, totalized to zero for nonintegrable inputs; the unconditional integral is likewise the library's totalized integral.