Lemma 18 — under Eq. (12), a consistent and generalizing rule is an AERM

Proved

LearnStability.Characterization.lemma18_consistent_generalizing_aerm

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$ . Suppose Equation (12) holds under $\mathcal D$ with rate $\varepsilon_{\rm emp}(m)$ , i.e.

\mathbb E_{S\sim\mathcal D^m}\bigl[|F_S(\hat h_S)-F^*|\bigr]\le\varepsilon_{\rm emp}(m)\qquad(m\ge1),

and that $A$ is $\varepsilon_{\rm cons}$ -consistent and $\varepsilon_{\rm gen}$ -generalizing under $\mathcal D$ . Then $A$ is an AERM under $\mathcal D$ with rate

\varepsilon_{\rm emp}(m)+\varepsilon_{\rm gen}(m)+\varepsilon_{\rm cons}(m).

Combined with Lemmas 16 and 20 this shows that a learnable problem has a universal AERM, the necessity 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 18 (p. 2653): if Equation (12) holds under `D` with rate `ε_emp`, i.e.
`E_{S∼D^m}[|F_S(ĥ_S) − F*|] ≤ ε_emp(m)` for all `m ≥ 1`, and a (measurable) rule `A` is
`ε_cons`-consistent and `ε_gen`-generalizing under `D`, then `A` is an AERM under `D` with
rate `ε_emp + ε_gen + ε_cons`. -/
theorem lemma18_consistent_generalizing_aerm {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] (εemp εcons εgen : ℕ → ℝ)
    (h12 : ∀ m : ℕ, 1 ≤ m →
      ∫ S, |ermValue f S - optRisk f D| ∂(sampleLaw D m) ≤ εemp m)
    (hcons : Consistent f A D εcons) (hgen : Generalizes f A D εgen) :
    IsAERM f A D (fun m => εemp m + εgen m + εcons m) := by sorry

end LearnStability.Characterization

Source

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

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$ .
Arbitrary functions $\varepsilon_{\rm emp},\varepsilon_{\rm cons},\varepsilon_{\rm gen}:\mathbb N\to\mathbb R$ .
For every $m\ge1$ ,

\int\big|\hat F_S-F^*_D\big|\,dD^m(S)\le\varepsilon_{\rm emp}(m),

where $F_D(h)=\int f(h;z)\,dD$ and $F^*_D=\inf_h F_D(h)$ .

$A$ is consistent under $D$ with rate $\varepsilon_{\rm cons}$ : $\int(F_D(A_m(S))-F^*_D)\,dD^m\le\varepsilon_{\rm cons}(m)$ for every $m\ge1$ .
$A$ generalizes under $D$ with rate $\varepsilon_{\rm gen}$ : $\int|F_D(A_m(S))-F_S(A_m(S))|\,dD^m\le\varepsilon_{\rm gen}(m)$ for every $m\ge1$ .

Conclusion. $A$ is an AERM under $D$ with rate $\varepsilon_{\rm emp}+\varepsilon_{\rm gen}+\varepsilon_{\rm cons}$ : for every $m\ge1$ ,

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

Degenerate cases.

If $Z$ is empty, the statement is vacuous.
$m=0$ is never tested.
None of the three rates is required to be monotone, vanishing or nonnegative.
The three hypotheses all concern the single fixed $D$ .
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