Theorem 1 — Tuned-step Convergence (positive denominators)

TunedConvexFedAvgConvergence 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$ with $\tau>0$ and $T>0$, and additionally require $D=\|x_0-x_\star\|>0$, $\sigma>0$, and $\zeta>0$. Set

where fractional powers are real powers. For $\eta=\eta_\star$ and the specified $\tau,T$, 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}$. The proposition states that every run with exactly this step size satisfies

There is no independently quantified step size or separate step-size inequality in this proposition: the run's step size is the displayed minimum. The assumptions make all four candidate step sizes positive and all displayed denominators nonzero. The implication makes no assertion for $D=0$, $\sigma=0$, or $\zeta=0$; in particular its $D>0$ premise is impossible in dimension $d=0$. It 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.