Utility Lemma 12 — the mean of m i.i.d. variables bounded by B deviates from its expectation by at most B/√m in L¹

Proved

LearnStability.ERMLOO.utility_lemma12

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

concentrationp2o-batch-p100bp2o-gran-per-chapterp2o-plan-paperp2o-v1probability

Let $X_1,\dots,X_m$ ( $m\ge1$ ) be independent, identically distributed real random variables on a probability space with $|X_i|\le B$ almost surely, and let $X=\frac1m\sum_{i=1}^m X_i$ . Then

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

This is the elementary concentration estimate used to compare the empirical risk of a fixed hypothesis with its risk, for instance in Lemma 14 and Lemma 16.

Formalization Note. The bound $|X_i|\le B$ is required almost surely (the paper writes $|X_i|\le B$ ), each $X_i$ is measurable, independence is iIndepFun, and identical distribution is required pairwise.

Preamble

import Mathlib

open MeasureTheory ProbabilityTheory

Formal statement

namespace LearnStability.ERMLOO

theorem utility_lemma12 {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω} [IsProbabilityMeasure μ]
    {m : ℕ} (hm : 1 ≤ m) (X : Fin m → Ω → ℝ) (B : ℝ)
    (hmeas : ∀ i, Measurable (X i))
    (hindep : iIndepFun X μ)
    (hident : ∀ i j, IdentDistrib (X i) (X j) μ μ)
    (hB : ∀ i, ∀ᵐ ω ∂μ, |X i ω| ≤ B) :
    ∫ ω, |(∑ i, X i ω) / m - ∫ ω', (∑ i, X i ω') / m ∂μ| ∂μ ≤ B / Real.sqrt m := by sorry

end LearnStability.ERMLOO

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

The setting is a probability space $(\Omega,\mu)$ , an integer $m \ge 1$ , and real-valued functions $X_1,\dots,X_m$ on $\Omega$ . Assume all of the following:

each $X_i$ is measurable;
$X_1,\dots,X_m$ are mutually independent under $\mu$ ;
for every pair $i,j$ , $X_i$ and $X_j$ have the same distribution under $\mu$ ;
for each $i$ , $|X_i(\omega)| \le B$ for $\mu$ -almost every $\omega$ , where $B$ is a real number.

Let $\bar X(\omega) = \frac1m\sum_{i=1}^m X_i(\omega)$ be the sample mean. The statement asserts

\int_\Omega \Big|\bar X(\omega) - \int_\Omega \bar X\,d\mu\Big|\,d\mu(\omega) \;\le\; \frac{B}{\sqrt m},

that is, $\mathbb{E}|\bar X - \mathbb{E}\bar X| \le B/\sqrt m$ .

Degenerate cases:

Sample size. $m = 0$ is excluded. For $m = 1$ the claim is $\mathbb{E}|X_1 - \mathbb{E}X_1| \le B$ .
Sign of $B$ . Because $\mu$ is a probability measure and $m \ge 1$ , the almost-sure bound forces $B \ge 0$ . With $B = 0$ , every $X_i$ is $0$ almost surely and both sides are $0$ .
Integrability. The integrands are measurable and bounded almost surely, so no zero-for-non-integrable convention is triggered.

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