Lemma 15 — an on-average generalizing AERM is consistent

Proved

LearnStability.Characterization.lemma15_aerm_onAverage_consistent

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

consistencylearning-theoryp2o-batch-p100bp2o-gran-per-chapterp2o-plan-paperp2o-v1

Let $f$ be a learning problem satisfying the standing assumptions, with $\mathcal H$ nonempty, $A$ a measurable learning rule and $\mathcal D$ a distribution on $\mathcal Z$ . If $A$ is an AERM with rate $\varepsilon_{\rm erm}(m)$ under $\mathcal D$ and on-average generalizes with rate $\varepsilon_{\rm oag}(m)$ under $\mathcal D$ , then $A$ is consistent under $\mathcal D$ with rate

\varepsilon_{\rm cons}(m)=\varepsilon_{\rm oag}(m)+\varepsilon_{\rm erm}(m),

that is, $\mathbb E_{S\sim\mathcal D^m}[F(A(S))-F^*]\le\varepsilon_{\rm oag}(m)+\varepsilon_{\rm erm}(m)$ for every $m\ge1$ .

With Lemma 11 and Claim 6 this gives the consistency part of Theorem 8 and the sufficiency direction of Theorem 7.

Preamble

import Mathlib
import Definitions.Def_LearnStability_Characterization_Setting
import Definitions.Def_LearnStability_Characterization_RuleProperties

open MeasureTheory

Formal statement

namespace LearnStability.Characterization

/-- Lemma 15 (p. 2651): if a (measurable) rule is an AERM with rate `ε_erm` and on-average
generalizes with rate `ε_oag` under `D`, then it is consistent with rate `ε_oag + ε_erm`
under `D`. -/
theorem lemma15_aerm_onAverage_consistent {H Z : Type*} [MeasurableSpace Z] [Nonempty H]
    (f : H → Z → ℝ) (B : ℝ) (hP : StandingAssumptions f B)
    (A : Rule H Z) (hA : MeasurableRule f A)
    (D : Measure Z) [IsProbabilityMeasure D] (εerm εoag : ℕ → ℝ)
    (haerm : IsAERM f A D εerm) (hoag : OnAverageGeneralizes f A D εoag) :
    Consistent f A D (fun m => εoag m + εerm m) := by sorry

end LearnStability.Characterization

Source

Shalev-Shwartz, Shamir, Srebro and Sridharan, Learnability, Stability and Uniform Convergence, JMLR 11 (2010), p. 2651, Lemma 15

Read-back

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

Hypotheses.

$H$ is nonempty.
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;
- $S\mapsto\hat F_S$ is measurable for each $m$ , where $\hat F_S=\inf_h F_S(h)$ and $F_S(h)=\frac1m\sum_i f(h;z_i)$ .
A rule $A$ with $(S,z)\mapsto f(A_m(S);z)$ jointly measurable for every $m$ .
A probability measure $D$ on $Z$ .
Two arbitrary functions $\varepsilon_{\rm erm},\varepsilon_{\rm oag}:\mathbb N\to\mathbb R$ .
$A$ is an AERM under $D$ with rate $\varepsilon_{\rm erm}$ : for every $m\ge1$ ,

\int\big(F_S(A_m(S))-\hat F_S\big)\,dD^m(S)\le\varepsilon_{\rm erm}(m).

$A$ on-average generalizes under $D$ with rate $\varepsilon_{\rm oag}$ : for every $m\ge1$ ,

\Big|\int\big(F_D(A_m(S))-F_S(A_m(S))\big)\,dD^m(S)\Big|\le\varepsilon_{\rm oag}(m),

where $F_D(h)=\int f(h;z)\,dD$ .

Conclusion. $A$ is consistent under $D$ with rate $\varepsilon_{\rm oag}+\varepsilon_{\rm erm}$ : for every $m\ge1$ ,

\int\big(F_D(A_m(S))-F^*_D\big)\,dD^m(S)\le\varepsilon_{\rm oag}(m)+\varepsilon_{\rm erm}(m),\qquad F^*_D=\inf_{h\in H}F_D(h).

Degenerate cases.

If $Z$ is empty, the statement is vacuous because there is no probability measure.
$H$ nonempty excludes the empty-infimum value.
The rates are not assumed to be monotone, to vanish, or to be nonnegative.
$m=0$ is never tested.
Non-integrable integrands would be read as $0$ .

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