Utility Lemma 12 — the sample mean of a bounded variable deviates by at most B/√m in expectation

Proved

LearnStability.Characterization.utility_lemma12

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

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

Let $\mathcal D$ be a probability distribution on $\mathcal Z$ and $g:\mathcal Z\to\mathbb R$ a measurable function with $|g(z)|\le B$ for all $z$ . For $m\ge1$ let $S=(z_1,\dots,z_m)\sim\mathcal D^m$ and $X=\frac1m\sum_{i=1}^m g(z_i)$ , so that $\mathbb E[X]=\mathbb E_{z\sim\mathcal D}[g(z)]$ . Then

\mathbb E\bigl[|X-\mathbb E[X]|\bigr]\le\frac{B}{\sqrt m}.

This is the only concentration fact used in the converse direction of Theorem 7 (Lemmas 16 and 20), where $g=f(h;\cdot)$ for a fixed hypothesis $h$ .

Formalization Note. The paper states the lemma for i.i.d. real variables $X_i$ with $|X_i|\le B$ . It is stated here for $X_i=g(z_i)$ , which is how the paper uses it; the two forms are equivalent (take $\mathcal Z=\mathbb R$ , $\mathcal D$ the common law, and $g$ the identity clipped to $[-B,B]$ ).

Preamble

import Mathlib
import Definitions.Def_LearnStability_Characterization_Setting

open MeasureTheory

Formal statement

namespace LearnStability.Characterization

/-- Utility Lemma 12 (p. 2650), for the sample average of a bounded measurable function:
if `|g(z)| ≤ B` for all `z` and `S = (z_1, …, z_m) ∼ D^m` with `m ≥ 1`, then
`E[|(1/m) ∑_i g(z_i) − E_D[g]|] ≤ B / √m`. -/
theorem utility_lemma12 {Z : Type*} [MeasurableSpace Z]
    (D : Measure Z) [IsProbabilityMeasure D]
    (g : Z → ℝ) (B : ℝ) (hg : Measurable g) (hB : ∀ z, |g z| ≤ B)
    (m : ℕ) (hm : 1 ≤ m) :
    ∫ S, |(∑ i, g (S i)) / m - ∫ z, g z ∂D| ∂(sampleLaw D m) ≤ B / Real.sqrt m := by sorry

end LearnStability.Characterization

Source

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

Read-back

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

This statement is about the sample average of a bounded function.

Hypotheses.

$Z$ is a measurable space and $D$ is a probability measure on $Z$ .
$g:Z\to\mathbb R$ is measurable.
$B\in\mathbb R$ satisfies $|g(z)|\le B$ for every $z\in Z$ .
$m\in\mathbb N$ with $m\ge1$ .

Conclusion. Let $S=(z_1,\dots,z_m)$ be drawn from the product law $D^m$ . Then

\int_{Z^m}\left|\frac1m\sum_{i=1}^m g(z_i)-\int_Z g\,dD\right|\,dD^m(S)\le\frac{B}{\sqrt m}.

Degenerate cases.

A probability measure exists only if $Z$ is nonempty, so the bound hypothesis forces $B\ge0$ .
$m=0$ is excluded, so $\sqrt m>0$ and no division-by-zero value arises.
$m=1$ is allowed, and then the bound is $B$ .
The integrals are Bochner integrals, which would be $0$ if the integrand were not integrable.

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