Proof of Theorem 11: $\mathbb E_S[(R - R_{\mathrm{emp}})^2] \le M^2/(2m) + 3M(\beta_1+\beta_2)$

Proved

StabGen.Hypothesis.second_moment_empirical

by mikedeng1 · Oct 4, 2026 · Mathlib 0df444a (Lean v4.33.1)

algorithmic-stabilitylearning-theoryp2o-batch-pfp1ap2o-gran-per-chapterp2o-plan-paperp2o-v1

Let $D$ be a probability distribution on $Z = X \times Y$ , let the cost satisfy $0 \le c(y', y) \le M$ , and let $A$ be a symmetric deterministic learning algorithm whose losses are measurable. Suppose that, at sample size $m \ge 2$ , $A$ has hypothesis stability $\beta_1$ and pointwise hypothesis stability $\beta_2$ . Then, with $S \sim D^m$ ,

\mathbb E_S\bigl[(R(A,S) - R_{\mathrm{emp}}(A,S))^2\bigr] \le \frac{M^2}{2m} + 3M(\beta_1 + \beta_2).

Chebyshev's inequality applied to this second-moment bound gives the empirical half of Theorem 11.

Formalization Note The paper prints $\frac{M^2}{2m} + 6M\beta_2$ , which follows from Lemma 9, eq. (8), and the printed bound $2\beta_2$ on the replace-one term. That bound is in fact $\beta_1 + \beta_2$ (see the preceding milestone), so the proven inequality is the one stated here; the two agree when $\beta_1 = \beta_2$ .

Preamble

import Mathlib
import Definitions.Def_FoundationsML_Stability_Loss
import Definitions.Def_FoundationsML_Stability_EmpiricalError
import Definitions.Def_FoundationsML_Stability_GeneralizationError
import Definitions.Def_StabGen_Hypothesis_Setting
import Definitions.Def_StabGen_Hypothesis_Stability

open MeasureTheory

Formal statement

namespace StabGen.Hypothesis

open FoundationsML.Stability

theorem second_moment_empirical {X Y Y' : Type*} [MeasurableSpace X] [MeasurableSpace Y]
    (D : Measure (X × Y)) [IsProbabilityMeasure D] (L : Y' → Y → ℝ) (M : ℝ)
    (hL : ∀ (y' : Y') (y : Y), 0 ≤ L y' y ∧ L y' y ≤ M)
    (A : LearningAlgorithm X Y Y')
    (hA : ∀ n : ℕ, Measurable (fun p : (Fin n → X × Y) × (X × Y) =>
      Loss L (A (trainingSet p.1)) p.2))
    (m : ℕ) (hm : 2 ≤ m) (β₁ β₂ : ℝ) (h₁ : HypothesisStable D L A m β₁)
    (h₂ : PointwiseHypothesisStable D L A m β₂) :
    ∫ S : Fin m → X × Y,
        (GeneralizationError D L (A (trainingSet S)) - EmpiricalError L S (A (trainingSet S))) ^ 2
      ∂(Measure.pi fun _ : Fin m => D)
    ≤ M ^ 2 / (2 * (m : ℝ)) + 3 * M * (β₁ + β₂) := by sorry

end StabGen.Hypothesis

Source

Bousquet & Elisseeff, Stability and Generalization, JMLR 2 (2002), p. 506, proof of Theorem 11 ("We thus get by (8)"; printed 6Mβ2 corrected to 3M(β1 + β2))

Human review

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

View graph

Proof of Theorem 11: ES[(R−Remp)2]≤M2/(2m)+3M(β1+β2)\mathbb E_S[(R - R_{\mathrm{emp}})^2] \le M^2/(2m) + 3M(\beta_1+\beta_2)ES​[(R−Remp​)2]≤M2/(2m)+3M(β1​+β2​)

Proof of Theorem 11: $\mathbb E_S[(R - R_{\mathrm{emp}})^2] \le M^2/(2m) + 3M(\beta_1+\beta_2)$