Eq. (6): the strongly convex empirical minimizer is replace-one stable, $|f(\hat h_S,z)-f(\hat h_S^{(i)},z)|\le 4L^2/(\lambda m)$

Proved

LearnStability.ConvexSCO.erm_replace_one_stability

by mikedeng1 · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

learning-theoryp2o-batch-p100bp2o-gran-per-chapterp2o-plan-paperp2o-v1stabilitystrong-convexity

Consider a stochastic convex optimization problem on $\mathcal H$ whose objective $f(h;z)$ is, for every $z$ , $\lambda$ -strongly convex ( $\lambda>0$ ) and $L$ -Lipschitz in $h\in\mathcal H$ . Let $S=(z_1,\dots,z_m)$ with $m\ge1$ , fix an index $i$ and a replacement instance $z'_i$ , and let $S^{(i)}$ be $S$ with $z_i$ replaced by $z'_i$ . Let $\hat h_S\in\mathcal H$ minimize $F_S$ over $\mathcal H$ and $\hat h_S^{(i)}\in\mathcal H$ minimize $F_{S^{(i)}}$ over $\mathcal H$ . Then

\forall z\in Z,\qquad \big|f(\hat h_S,z)-f(\hat h_S^{(i)},z)\big|\ \le\ \frac{4L^2}{\lambda m}.

This is a deterministic statement: it holds for every sample and every replacement. It says that empirical minimization of a strongly convex objective is uniform-RO stable with rate $4L^2/(\lambda m)$ .

Formalization Note The paper's stochastic convex optimization standing assumptions (closed, bounded $\mathcal H$ , $|f|\le C$ , measurability) are carried in the hypothesis bundle although this step does not use them.

Preamble

import Mathlib
import Definitions.Def_LearnStability_ConvexSCO_Setting
import Definitions.Def_LearnStability_ConvexSCO_Problem

Formal statement

namespace LearnStability.ConvexSCO

/-- Eq. (6), proof of Theorem 2 (p. 2645): in a stochastic convex optimization problem whose
objective is `λ`-strongly convex (`λ > 0`) and `L`-Lipschitz in `h` on `H`, let `ĥ_S` minimize
the empirical risk `F_S` over `H` and let `ĥ_S^{(i)}` minimize the empirical risk of the sample
`S^{(i)}` obtained by replacing the `i`-th instance of `S` by `z'_i`. Then for every
`z ∈ Z`, `|f(ĥ_S, z) − f(ĥ_S^{(i)}, z)| ≤ 4L²/(λm)`. -/
theorem erm_replace_one_stability {Z E : Type*} [MeasurableSpace Z] [NormedAddCommGroup E]
    [InnerProductSpace ℝ E] [CompleteSpace E] {Hset : Set E} {f : E → Z → ℝ} {L C lam : ℝ}
    (hP : IsStochasticConvexProblem Hset f L C) (hlam : 0 < lam)
    (hsc : ∀ z, StrongConvexOn Hset lam (fun h => f h z))
    {m : ℕ} (hm : 1 ≤ m) (S : Fin m → Z) (i : Fin m) (z'_i : Z) {hS hSi : E}
    (hS_mem : hS ∈ Hset) (hS_min : ∀ h ∈ Hset, empRisk f S hS ≤ empRisk f S h)
    (hSi_mem : hSi ∈ Hset)
    (hSi_min : ∀ h ∈ Hset,
      empRisk f (Function.update S i z'_i) hSi ≤ empRisk f (Function.update S i z'_i) h) :
    ∀ z : Z, |f hS z - f hSi z| ≤ 4 * L ^ 2 / (lam * m) := by sorry

end LearnStability.ConvexSCO

Source

Shalev-Shwartz, Shamir, Srebro and Sridharan, Learnability, Stability and Uniform Convergence, JMLR 11 (2010), p. 2645, Eq. (6) (proof of Theorem 2)

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

Setting. $E$ is a complete real inner product space, $Z$ is a measurable space, $\mathcal H \subseteq E$ , $f : E \times Z \to \mathbb{R}$ , and $L, C, \lambda \in \mathbb{R}$ .

Hypothesis 1: $(\mathcal H, f, L, C)$ is a stochastic convex optimization problem.

$\mathcal H$ is nonempty, convex, closed and norm-bounded.
Each $z \mapsto f(h; z)$ with $h \in \mathcal H$ is measurable.
$|f(h; z)| \le C$ on $\mathcal H \times Z$ .
Each $h \mapsto f(h; z)$ is convex on $\mathcal H$ .
$L \ge 0$ , and $|f(h;z) - f(h';z)| \le L\|h - h'\|$ for all $z$ and $h, h' \in \mathcal H$ .

Hypothesis 2: strong convexity. $\lambda > 0$ , and for every $z \in Z$ the map $h \mapsto f(h; z)$ is $\lambda$ -strongly convex on $\mathcal H$ . That is, for $x, y \in \mathcal H$ and $a, b \ge 0$ with $a + b = 1$ :

f(ax+by; z) \le a f(x;z) + b f(y;z) - ab\frac{\lambda}{2}\|x-y\|^2.

Hypothesis 3: the two samples. $m \ge 1$ is a natural number, $S \in Z^m$ , $i \in \{1,\dots,m\}$ and $z'_i \in Z$ . $S^{(i)}$ is $S$ with its $i$ -th entry replaced by $z'_i$ .

Hypothesis 4: the two minimizers. With $F_S(h) = \frac1m\sum_{j=1}^m f(h; S_j)$ :

$\hat h_S \in \mathcal H$ satisfies $F_S(\hat h_S) \le F_S(h)$ for all $h \in \mathcal H$ .
$\hat h_S^{(i)} \in \mathcal H$ satisfies $F_{S^{(i)}}(\hat h_S^{(i)}) \le F_{S^{(i)}}(h)$ for all $h \in \mathcal H$ .

Conclusion. For every $z \in Z$ :

\big|f(\hat h_S; z) - f(\hat h_S^{(i)}; z)\big| \le \frac{4L^2}{\lambda m}.

Degenerate cases.

$m = 0$ : excluded.
$Z$ nonempty: forced, because $S$ exists with $m \ge 1$ .
$\mathcal H$ a single point: both minimizers coincide and the conclusion is $0 \le 4L^2/(\lambda m)$ .
$L = 0$ : the Lipschitz condition with constant $0$ together with $\lambda > 0$ strong convexity forces $\mathcal H$ to be a single point, so the statement reduces to the previous case.
$z'_i = S_i$ : $S^{(i)} = S$ , but the two minimizers are still arbitrary minimizers of the same function.
Unused data: $C$ enters only through the structure hypothesis. No measure appears.

Human review

Endorsed by Shuze Chen · Sep 27, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Sep 27, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Eq. (6): the strongly convex empirical minimizer is replace-one stable, ∣f(h^S,z)−f(h^S(i),z)∣≤4L2/(λm)|f(\hat h_S,z)-f(\hat h_S^{(i)},z)|\le 4L^2/(\lambda m)∣f(h^S​,z)−f(h^S(i)​,z)∣≤4L2/(λm)

Eq. (6): the strongly convex empirical minimizer is replace-one stable, $|f(\hat h_S,z)-f(\hat h_S^{(i)},z)|\le 4L^2/(\lambda m)$