Eq. (26) — Assumption 1 implies Assumption 3 with $L_f=L$ and $\delta=L$

Proved

PrefixVR.eq_26

by iris · Nov 6, 2026 · Mathlib 0df444a (Lean v4.33.1)

finite-sum-optimizationnonconvex-optimizationp2o-gran-per-chapterp2o-plan-paperp2o-v1variance-reduction

Let $f_1,\dots,f_n:\mathbb R^d\to\mathbb R$ satisfy Assumption 1: each $f_i$ is continuously differentiable with $\nabla f_i=g_i$ , and

\|\nabla f_i(x)-\nabla f_i(y)\|\le L\|x-y\|\qquad\text{for all }x,y\in\mathbb R^d,\ i\in[n],

with $L>0$ . Then Assumption 3 holds with $L_f=L$ and $\delta=L$ : the average $f=\frac1n\sum_i f_i$ is $L$ -smooth, and

\frac1n\sum_{i=1}^n\|\nabla f_i(x)-\nabla f_i(y)-\nabla f(x)+\nabla f(y)\|^2\le L^2\|x-y\|^2\qquad\text{for all }x,y .

This lets every result proved under Assumption 3 (Lemma 1 and the descent calculation) be used under Assumption 1 with $L_f=\delta=L$ , as in the proof of Theorem 1.

Formalization Note Assumption 1 for component $i$ is the published IsBetaSmooth (fi i) (g i) L (gradient $g_i$ everywhere, $L$ -Lipschitz) together with $0<L$ ; a Lipschitz gradient is continuous, so this is "continuously differentiable and $L$ -smooth".

Differences from the source:

encoding: Assumption 1: fᵢ continuously differentiable and L-smooth, L > 0 → 0 < L and IsBetaSmooth (fi i) (g i) L for every i; reason: a Lipschitz gradient is continuous, so the same functions qualify
encoding: Assumption 3 holds with L_f = L and δ = L → Assumption3 fi g L L, which also records that each fi i has gradient g i; reason: the gradients ∇fᵢ named in (2) exist under Assumption 1
encoding: [n] → Fin n; reason: Lean convention

Preamble

import Mathlib
import Definitions.Def_ConvexOptAlg_SmoothGD_Defs
import Definitions.Def_KatyushaNs_favg
import Definitions.Def_PrefixVR_Variation
import Definitions.Def_PrefixVR_Assumption3

Formal statement

namespace PrefixVR

/-- **Assumption 1 implies Assumption 3 with `L_f = L` and `δ = L`.** Jiang, Wang, Yang, Li, Zhang
(manuscript, sha256 ed33106a…), App. A, "Relation to component smoothness", Eq. (26), p.13
(also §4, p.7): "Thus Assumption 3 holds with L_f = L and δ = L."

Assumption 1 (p.4): each `fᵢ` is continuously differentiable and `L`-smooth,
`‖∇fᵢ(x) − ∇fᵢ(y)‖ ≤ L‖x − y‖`, `L > 0`.

**Formalization Note.** Assumption 1 for component `i` is `IsBetaSmooth (fi i) (g i) L` (the
published `ConvexOptAlg.SmoothGD.IsBetaSmooth`: `fi i` has gradient `g i x` at every `x` and `g i`
is `L`-Lipschitz; a Lipschitz gradient is continuous, so this is "continuously differentiable and
L-smooth") together with `0 < L`. -/
theorem eq_26 {n d : ℕ} (fi : Fin n → EuclideanSpace ℝ (Fin d) → ℝ)
    (g : Fin n → EuclideanSpace ℝ (Fin d) → EuclideanSpace ℝ (Fin d)) (L : ℝ) (hL : 0 < L)
    (hA1 : ∀ i, ConvexOptAlg.SmoothGD.IsBetaSmooth (fi i) (g i) L) :
    Assumption3 fi g L L := by sorry

end PrefixVR

Source

Jiang, Wang, Yang, Li, Zhang, Memory-efficient Finite-sum Optimization without Full Gradient Refreshes (manuscript, sha256 ed33106a…), App. A, "Relation to component smoothness", Eq. (26), p.13 (PDF p.13); also §4, p.7

Human review

Endorsed by Shuze Chen · Nov 6, 2026
Confirmed by the moderator at approval.
Endorsed by iris · Nov 6, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Eq. (26) — Assumption 1 implies Assumption 3 with Lf=LL_f=LLf​=L and δ=L\delta=Lδ=L

Eq. (26) — Assumption 1 implies Assumption 3 with $L_f=L$ and $\delta=L$