Claim 6 — uniform-RO stability implies average-RO stability with the same rate

Proved

LearnStability.Characterization.claim6_uniformRO_imp_averageRO

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

learning-theoryp2o-batch-p100bp2o-gran-per-chapterp2o-plan-paperp2o-v1stability

Let $f$ be a learning problem satisfying the standing assumptions and $A$ a measurable learning rule. If $A$ is uniform-RO stable with rate $\varepsilon_{\rm stable}(m)$ , then for every probability distribution $\mathcal D$ on $\mathcal Z$ it is average-RO stable with rate $\varepsilon_{\rm stable}(m)$ under $\mathcal D$ :

\Bigl|\frac1m\sum_{i=1}^m\mathbb E\bigl[f(A(S^{(i)});z_i')-f(A(S);z_i')\bigr]\Bigr|\le\varepsilon_{\rm stable}(m)\qquad(m\ge1).

The implication is not a direct specialisation: Definition 4 uses one test point $z'$ for all $i$ , whereas Definition 5 tests at the replacement point $z_i'$ . Claim 6 lets the sufficiency direction of Theorem 7 use the in-expectation machinery of Lemmas 11 and 15.

Formalization Note. The paper states Claim 6 without proof and without quantifying the distribution; it is read as holding under every distribution (the paper calls this "universally" stable, p. 2648).

Preamble

import Mathlib
import Definitions.Def_LearnStability_Characterization_Setting
import Definitions.Def_LearnStability_Characterization_RuleProperties
import Definitions.Def_LearnStability_Characterization_Stability

open MeasureTheory

Formal statement

namespace LearnStability.Characterization

/-- Claim 6 (p. 2648): a (measurable) rule that is uniform-RO stable with rate `ε` is
average-RO stable with rate `ε` under every distribution `D`. -/
theorem claim6_uniformRO_imp_averageRO {H Z : Type*} [MeasurableSpace Z]
    (f : H → Z → ℝ) (B : ℝ) (hP : StandingAssumptions f B)
    (A : Rule H Z) (hA : MeasurableRule f A) (ε : ℕ → ℝ)
    (hstab : UniformROStable f A ε) :
    ∀ D : Measure Z, IsProbabilityMeasure D → AverageROStable f A D ε := by sorry

end LearnStability.Characterization

Source

Shalev-Shwartz, Shamir, Srebro and Sridharan, Learnability, Stability and Uniform Convergence, JMLR 11 (2010), p. 2648, Claim 6

Read-back

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

Hypotheses.

A loss $f$ $f$ and a real number $B$ $B$ satisfying the standing assumptions:
- $|f(h;z)|\le B$ ;
- each $f(h;\cdot)$ is measurable;
- for each $m$ , the minimal empirical risk $S\mapsto\inf_h\frac1m\sum_i f(h;z_i)$ is measurable.
A rule $A$ with $(S,z)\mapsto f(A_m(S);z)$ jointly measurable for every $m$ .
An arbitrary $\varepsilon:\mathbb N\to\mathbb R$ .
$A$ is uniform-RO stable with rate $\varepsilon$ : for every $m\ge1$ , all $S,S'\in Z^m$ and every $z'\in Z$ ,

\frac1m\sum_{i=1}^m\big|f(A_m(S^{(i)});z')-f(A_m(S);z')\big|\le\varepsilon(m).

Conclusion. For every probability measure $D$ on $Z$ , $A$ is average-RO stable under $D$ with the same $\varepsilon$ : for every $m\ge1$ ,

\Big|\frac1m\sum_{i=1}^m\int\big(f(A_m(S^{(i)});z'_i)-f(A_m(S);z'_i)\big)\,d(D^m\otimes D^m)(S,S')\Big|\le\varepsilon(m).

Degenerate cases.

If $Z$ is empty, the conclusion is vacuous because there is no probability measure. The uniform-stability hypothesis is also vacuous in that case.
If $H$ is empty, no rule exists and the statement is vacuous.
$\varepsilon$ is not assumed to be a rate, and $\varepsilon(0)$ is never used.

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