LemmaStatement: 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.

Quadratic-weighted telescope for a strongly convex recursion

Statement

Let $μ > 0$ , $a \geq 4$ , $T \geq 1$ , and $η_{t} = \frac{4}{μ (a + t)}, w_{t} = (a + t)^{2}, S_{T} = \sum_{t = 0}^{T - 1} w_{t} .$ Suppose nonnegative sequences $u_{t}, e_{t}$ satisfy, for $0 \leq t < T$ , $u_{t + 1} \leq (1 - μ η_{t}) u_{t} - A η_{t} e_{t} + B η_{t}^{2} + C η_{t}^{3}$ with $A > 0$ and $B, C \geq 0$ . Then $\frac{A}{S_{T}} \sum_{t = 0}^{T - 1} w_{t} e_{t} \leq \frac{μ a^{3}}{4 S_{T}} u_{0} + \frac{2 T (T + 2 a)}{μ S_{T}} B + \frac{16 T}{μ^{2} S_{T}} C .$ Also $S_{T} \geq T^{3} / 3$ .

Facts & Assumptions

Given: The scalar recurrence and parameters in the Statement.

[A1]

$u_{t}, e_{t}$ are nonnegative; $A > 0$ , $B, C \geq 0$ , $μ > 0$ , $a \geq 4$ .

Proof

1.1A1algebra

Since $w_{t} / η_{t} = μ (a + t)^{3} / 4$ , for $1 \leq t < T$ , [given] $(1 - μ η_{t}) \frac{w_{t}}{η_{t}} = \frac{μ}{4} (a + t - 4) (a + t)^{2} \leq \frac{μ}{4} (a + t - 1)^{3} = \frac{w_{t - 1}}{η_{t - 1}} .$ The inequality follows by expanding the difference: $(a + t - 1)^{3} - (a + t - 4) (a + t)^{2} = a^{2} + 2 a t + t^{2} + 3 a + 3 t - 1 \geq 0$ for $a \geq 4$ . At $t = 0$ , $(1 - μ η_{0}) w_{0} / η_{0} = μ a^{2} (a - 4) / 4 \leq μ a^{3} / 4$ .

1.2step 1.1A1algebra

Multiply each recurrence by the positive number $w_{t} / η_{t}$ and use [given] step 1.1 to telescope the $u_{t}$ terms. Dropping the nonnegative terminal term yields $A \sum_{t = 0}^{T - 1} w_{t} e_{t} \leq \frac{μ a^{3}}{4} u_{0} + B \sum_{t = 0}^{T - 1} w_{t} η_{t} + C \sum_{t = 0}^{T - 1} w_{t} η_{t}^{2} .$ Direct summation gives $\sum w_{t} η_{t} = 2 T (T + 2 a - 1) / μ \leq 2 T (T + 2 a) / μ$ and $\sum w_{t} η_{t}^{2} = 16 T / μ^{2}$ .

2.1step 1.2A1algebra∎

Divide step 1.2 by $S_{T}$ to obtain the stated bound. Since $a \geq 4$ , $S_{T} \geq \sum_{t = 0}^{T - 1} (t + 1)^{2} = T (T + 1) (2 T + 1) / 6 \geq T^{3} / 3$ .

Used by

Strongly convex local-SGD round complexity Theorem

Dependency tree · 0 levels

Nothing. This result depends on no other item in the library.

Sources

Sebastian U. Stich, Local SGD Converges Fast and Communicates Little, Lemma 3.4 and Appendix A (standard reference, not scraped)