TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Expected generalization from uniform stability

Statement

Let $(X, Σ_{X})$ and $(Y, Σ_{Y})$ be nonempty measurable instance and label spaces, and equip $Z = X \times Y$ with $Σ_{Z} = Σ_{X} \otimes Σ_{Y}$ . Let $P$ be a probability measure on $(Z, Σ_{Z})$ , let $F$ be a nonempty class of measurable functions $f : (X, Σ_{X}) \to (R, B (R))$ , and let $ℓ : R \times Y \to [0, \infty)$ be measurable with respect to $B (R) \otimes Σ_{Y}$ . For $f \in F$ and $z = (x, y)$ write $L_{f} (z) = ℓ (f (x), y)$ , $R_{P} (f) = \int_{Z} L_{f} (z) P (d z)$ , and ${\hat{R}}_{S} (f) = m^{- 1} \sum_{i = 1}^{m} L_{f} (Z_{i})$ . Let $S = (Z_{1}, \dots, Z_{m})$ have product law $P^{m}$ on $(Z^{m}, Σ_{Z}^{\otimes m})$ , with $m \geq 1$ , and let $A$ be a deterministic, permutation-invariant size-indexed learning rule that outputs members of $F$ and assume the maps $(S, z) \mapsto L_{A_{S}} (z)$ and $(S, z) \mapsto L_{A_{S ∖ i}} (z)$ for every $i \in [m]$ are jointly measurable with respect to $Σ_{Z}^{\otimes m} \otimes Σ_{Z}$ . Assume also that the sample-dependent risk, empirical-risk, and leave-one-out maps in the conclusions are measurable. Assume $0 \leq L_{A_{T}} (z) \leq M < \infty$ for every full or deleted sample $T$ and every $z \in Z$ , and assume $A$ has uniform deletion stability with a finite nonincreasing sequence $(β_{n})_{n \geq 1}$ . Define $R_{l o o} (A, S) = m^{- 1} \sum_{i = 1}^{m} L_{A_{S ∖ i}} (Z_{i})$ , using the size- $m$ deletion output. Then

$E_{S \sim P^{m}} [R_{P} (A_{S}) - {\hat{R}}_{S} (A_{S})] \leq 2 β_{m} and E_{S \sim P^{m}} [R_{P} (A_{S}) - R_{l o o} (A, S)] \leq β_{m} .$

Moreover, for every sample $S$ and index $i \in [m]$ ,

$∣ R_{P} (A_{S}) - R_{P} (A_{S ∖ i}) ∣ \leq β_{m} .$

All three conclusions are choice-free.

Statement references

Bousquet and Elisseeff, Lemma 7 and proof, printed pp. 504–505, give the expected generalization and leave-one-out identities under the deletion convention. Full JMLR paper PDF

Mohri, Rostamizadeh, and Talwalkar, Theorem 14.2 and complete proof, printed pp. 334–336, give the corresponding replacement-stability argument. Full second-edition book PDF

Facts & Assumptions

Given: A supervised prediction problem with law $P$ , an IID product sample $S \sim P^{m}$ , a measurable size-indexed learning rule, bounded measurable losses, and uniform deletion-stability coefficient $β_{m}$ .

[F1]

A supervised prediction problem fixes measurable instance and label spaces, a joint sample law, a class of measurable predictors, and a measurable loss. Supervised prediction problems

[F2]

Population risk is the integral of the predictor's loss against $P$ , and empirical risk is the finite average of its sample losses. Population and empirical risk

[F3]

IID means mutually independent random elements with the same law; here the coordinate sample is the finite product sample with common law $P$ . Identical distribution and IID families

[F4]

The finite product sigma-algebra is generated by coordinate rectangles; finite product measures have the rectangle formula and are unique, so permuting coordinates preserves the product law. The product sigma-algebra and its finite iterates For sigma-finite factors, the product measure exists, has the rectangle formula, is sigma-finite, and is unique

[F5]

For integrable measurable functions on a product, the product integral equals the iterated section integrals. Fubini's theorem for L^1 functions on a sigma-finite product

[F6]

A measurable function is in $L^{1}$ when its absolute value has finite integral; the stated uniform bound on a probability product gives this integrability. Integrable real and complex functions, and their integrals

[F7]

The integral is linear on $L^{1}$ . The Lebesgue integral is linear on $L^{1} (μ)$

[F8]

For $h \in L^{1}$ , $∣ \int h d P ∣ \leq \int ∣ h ∣ d P$ . The modulus of an integral is bounded by the integral of the modulus

[F9]

Uniform deletion stability bounds the loss change between the full output and its size- $m$ deleted output by $β_{m}$ , uniformly over samples, deleted indices, and test points. Uniform algorithmic stability under deletion

[A1]

The sample-dependent loss and risk maps are jointly measurable and all losses used here lie in $[0, M]$ .

Proof

1.1A1F1F2F3F4F5F6givenconstruct

Fix $i \in [m]$ and extend the coordinate sample to $(Z^{m + 1}, P^{m + 1})$ , writing $Z_{i}^{'}$ for the last coordinate. By [A1] and [F6], $(S, z^{'}) \mapsto L_{A_{S}} (z^{'})$ is integrable on this product space, and [F5] identifies $E_{S} R_{P} (A_{S})$ with $E_{S, Z_{i}^{'}} L_{A_{S}} (Z_{i}^{'})$ . On each all-coordinate rectangle, the $P^{m + 1}$ mass is the product of its coordinate masses. Transposing coordinates $i$ and $m + 1$ preserves that value; the generating and uniqueness statements in [F4] therefore show that the transposed product law is again $P^{m + 1}$ . If $S^{(i)}$ replaces $Z_{i}$ by $Z_{i}^{'}$ , this gives $E_{S, Z_{i}^{'}} L_{A_{S}} (Z_{i}^{'}) = E_{S, Z_{i}^{'}} L_{A_{S^{(i)}}} (Z_{i})$ .

1.2A1F2F7F8F9given

By [F2] and [F7], $R_{P} (A_{S}) - R_{P} (A_{S ∖ i}) = \int_{Z} (L_{A_{S}} (z) - L_{A_{S ∖ i}} (z)) P (d z)$ . The integrand has absolute value at most $β_{m}$ by [F9], so [F8] gives $∣ R_{P} (A_{S}) - R_{P} (A_{S ∖ i}) ∣ \leq \int β_{m} d P = β_{m}$ .

1.3A1F3F4F5F6F7givenconstruct

For each $i$ , the deleted output $A_{S ∖ i}$ depends only on the retained coordinates. Since $Z_{i}$ is independent of them and has law $P$ , [F5] and [F6] give $E_{S} L_{A_{S ∖ i}} (Z_{i}) = E_{S} R_{P} (A_{S ∖ i})$ . Averaging over $i$ therefore yields $E_{S} [R_{P} (A_{S}) - R_{l o o} (A, S)] = m^{- 1} \sum_{i = 1}^{m} E_{S} [R_{P} (A_{S}) - R_{P} (A_{S ∖ i})]$ .

2.1F2F9step 1.1algebra

By [F2] and linearity, step 1.1 gives $E_{S} [R_{P} (A_{S}) - {\hat{R}}_{S} (A_{S})] = m^{- 1} \sum_{i = 1}^{m} E_{S, Z_{i}^{'}} [L_{A_{S^{(i)}}} (Z_{i}) - L_{A_{S}} (Z_{i})]$ . The indexed retained samples $S ∖ i$ and $S^{(i)} ∖ i$ coincide. Applying [F9] to each full output and that common deletion output, then the triangle inequality, bounds the absolute value of every summand by $2 β_{m}$ . Averaging gives the first expected bound.

3.1step 1.2step 1.3algebra∎

Each summand in the average in step 1.3 is at most $β_{m}$ by step 1.2, so its average is at most $β_{m}$ . This proves the leave-one-out bound.

Depends on

Used by

High-probability generalization from uniform stability Theorem

Dependency tree · two levels

38 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Olivier Bousquet and André Elisseeff, Stability and Generalization, JMLR 2 (2002), Lemma 7 and proof (standard reference, not scraped)
Mehryar Mohri, Afshin Rostamizadeh, and Ameet Talwalkar, Foundations of Machine Learning, 2nd ed., Theorem 14.2 and proof (standard reference, not scraped)