TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generated

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Strongly convex FedAvg under bounded gradient dissimilarity

Statement

Assume the Axiom of Choice. Let $N, d, K, R \geq 1$ be positive integers and $1 \leq S \leq N$ . Let $f_{i} : R^{d} \to R$ be differentiable, $μ$ -strongly convex and $β$ -smooth, with $0 < μ \leq β$ , and let $f = N^{- 1} \sum_{i = 1}^{N} f_{i}$ attain its minimum $f^{⋆} = f (x^{⋆})$ . Assume fresh conditionally unbiased local stochastic gradients with within-client conditional variance at most $σ^{2}$ , independent of the fresh client sample. The conditional mean and variance bounds hold given the full prequery history, including the round-start history, the revealed client sample and all earlier oracle draws from every client in a fixed chronological ordering, also for the hypothetical client paths used in the analysis. For constants $B \geq 1$ and $G \geq 0$ , assume the convex-client gradient-dissimilarity bound $\frac{1}{N} \sum_{i = 1}^{N} ∥ \nabla f_{i} (x) ∥_{2}^{2} \leq G^{2} + 2 β B^{2} (f (x) - f^{⋆}) (x \in R^{d}) .$ Alternatively, assume the standard $(G, B)$ -bounded gradient-dissimilarity condition $\frac{1}{N} \sum_{i} ∥ \nabla f_{i} (z) ∥_{2}^{2} \leq G^{2} + B^{2} ∥ \nabla f (z) ∥_{2}^{2} (z \in R^{d}) .$ Either assumption gives all the conclusions below with the same $G, B$ and stepsize restrictions. Run the uniform-client analysis mode of FedAvg with $1 \leq S \leq N$ clients sampled uniformly without replacement per round and $K \geq 1$ local steps. Choose $η_{g} = \sqrt{S}$ and $0 < \tilde{η} = K η_{l} η_{g} \leq \frac{1}{32 (B^{2} + 1) β} .$ At round $r$ , let $x_{r}$ be the server iterate and set $λ = \frac{μ \tilde{η}}{2}, W_{R} = \sum_{r = 1}^{R} (1 - λ)^{- r} .$ Choose an independent index $J \in {1, \dots, R}$ with probability $\Pr (J = r) = (1 - λ)^{- r} / W_{R}$ and return ${\overset{ˉ}{x}}_{R} = x_{J - 1}$ . Then $E [f ({\overset{ˉ}{x}}_{R}) - f^{⋆}] \leq \frac{3 ∥ x_{0} - x^{⋆} ∥_{2}^{2}}{\tilde{η} W_{R}} + 3 \tilde{η} (\frac{11 σ^{2}}{2 K S} + 8 (1 - \frac{S}{N}) \frac{G^{2}}{S}) + 54 β G^{2} {\tilde{η}}^{2} .$ In particular, for target $ϵ > 0$ , a choice of $\tilde{η}$ no larger than $[32 (B^{2} + 1) β]^{- 1}$ and $R = O ⁣ ([\frac{(B^{2} + 1) β}{μ} + \frac{σ^{2}}{μ K S ϵ} + \frac{(1 - S / N) G^{2}}{μ S ϵ} + \frac{\sqrt{β} G}{μ \sqrt{ϵ}}] \log (2 + \frac{μ ∥ x_{0} - x^{⋆} ∥_{2}^{2}}{ϵ}))$ suffice to ensure $E [f ({\overset{ˉ}{x}}_{R}) - f^{⋆}] \leq ϵ$ , with a universal constant in the $O (\cdot)$ notation. This is an equal-client strongly convex rate; it does not apply to the count-weighted deployment objective without a separate weighted analysis.

Statement references

Standard and gap forms of bounded client gradient dissimilarity

Standard client dissimilarity implies the gap form with unchanged parameters

Karimireddy et al., SCAFFOLD, Theorem I and Appendix D.3, Lemmas 7–8

Facts & Assumptions

Given: The client objectives, stochastic-gradient process, FedAvg output and sampling law in the Statement.

[F1]

One-round progress of strongly convex FedAvg: with $\tilde{η}$ as above, one round gives distance contraction, a negative objective-gap term, sampling variance and client-drift error.

[F2]

Client drift under FedAvg gradient dissimilarity: the local-drift error is bounded by a fraction of the objective gap, a stochastic-gradient term and a cubic $G^{2}$ term.

[F3]

Geometric and sublinear averaging for descent recursions: the geometric weighted average of a strongly convex descent recursion bounds its expected objective gap.

[F4]

Federated objectives and client sampling and Federated averaging (FedAvg): the analyzed objective is $N^{- 1} \sum_{i} f_{i}$ , with each round sampling a uniform fixed-size client subset and averaging selected model differences.

[F5]

Moments of a uniformly sampled fixed-size client set: fixed-size sampling is unbiased and its exact finite-population variance is at most twice the population second moment times $(1 - S / N) / S$ .

[F6]

Smooth convex gradient differences around a minimizer and Gradient of a finite sum is the finite sum of gradients: convex $β$ -smooth clients satisfy the required gradient-second-moment estimate around a minimizer, and their average gradient is $\nabla f$ .

[F7]

The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ : squared distances expand by bilinearity.

[F8]

Filtration and filtered probability space, Conditional expectation as an ae class, Basic algebra and order properties of conditional expectation, Taking out what is known, Expectation of a nonnegative or integrable random variable, and Linearity, monotonicity, and the modulus bound for expectation: roundwise conditional expectations are linear, obey the tower rule and preserve nonnegative integrable inequalities.

[F9]

Standard client dissimilarity implies the gap form with unchanged parameters: under the stated common smoothness and attained finite minimum, the standard condition implies the displayed gap form with unchanged $G, B$ .

[A1]

The conditional stochastic-gradient hypotheses and bounded gradient-dissimilarity assumption in the Statement hold at every round and query point.

[A2]

Assume the Axiom of Choice. It is used only to invoke the published conditional-expectation-as-an-a.e.-class interface in [F8].

Proof

1.1F9F1F2F4F5F6F7F8A1A2givenalgebra

In the standard-condition branch, [F9] supplies the displayed gap-form assumption with unchanged $G, B$ ; in the original gap-form branch it is already assumed. Let $d_{r} = E ∥ x_{r} - x^{⋆} ∥_{2}^{2}$ and [given] $q_{r - 1} = E [f (x_{r - 1}) - f^{⋆}]$ . Apply [F1] and then [F2] with $η_{g} = \sqrt{S}$ . Their gap terms combine to $- \tilde{η} q_{r - 1} / 3$ . The resulting recurrence is $d_{r} \leq (1 - λ) d_{r - 1} - \frac{\tilde{η}}{3} q_{r - 1} + b {\tilde{η}}^{2} + c {\tilde{η}}^{3}, b = \frac{11 σ^{2}}{2 K S} + 8 (1 - \frac{S}{N}) \frac{G^{2}}{S}, c = 18 β G^{2} .$ Indeed the stochastic terms are $5 σ^{2} / (K S) + σ^{2} / (2 K η_{g}^{2}) = 11 σ^{2} / (2 K S)$ because $η_{g}^{2} = S$ ; the sampling term is the one in [F1], and the remaining drift term is $18 β G^{2} {\tilde{η}}^{3}$ .

2.1step 1.1F3givenalgebra

Apply [F3] to step 1.1 with $a = 1 / 3$ , $ρ = μ / 2$ , and weights $w_{r} = (1 - λ)^{- r}$ . It yields $E [f ({\overset{ˉ}{x}}_{R}) - f^{⋆}] \leq \frac{3 d_{0}}{\tilde{η} W_{R}} + 3 b \tilde{η} + 3 c {\tilde{η}}^{2},$ which is the displayed bound after substituting $b, c$ .

3.1F3step 1.1step 2.1givenalgebra∎

Write $D = ∥ x_{0} - x^{⋆} ∥_{2}$ . Since [given] $W_{R} = ((1 - λ)^{- R} - 1) / λ$ , the first term in step 2.1 is at most $ϵ / 3$ whenever $R \geq \frac{2}{μ \tilde{η}} \log (1 + \frac{9 μ D^{2}}{2 ϵ}) .$ This follows from $- \log (1 - λ) \geq λ$ . Choose $\tilde{η}$ not exceeding the minimum of $[32 (B^{2} + 1) β]^{- 1}$ , $ϵ / (9 b)$ when $b > 0$ , and $\sqrt{ϵ / (162 β G^{2})}$ when $G > 0$ ; omit a bound whose denominator is zero. Then each of the last two terms in step 2.1 is at most $ϵ / 3$ . Taking the least integer $R$ satisfying the preceding display gives the claimed communication-round bound: the reciprocal step is bounded by a constant times $(B^{2} + 1) β + b / ϵ + \sqrt{β} G / \sqrt{ϵ}$ , divided by $μ$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

65 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Sai Praneeth Karimireddy et al., SCAFFOLD, Theorem I (strongly convex branch), Appendix D.3, Lemmas 7–8 (standard reference, not scraped)