TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck pass

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.

One-sided coordinate Rademacher contraction

Statement

Let $m \geq 1$ , let $z_{1}, \dots, z_{m}$ be fixed, and let $F$ be a nonempty finite class of real-valued functions on their domain. For each $i$ , let $Φ_{i} : R \to R$ satisfy $∣ Φ_{i} (x) - Φ_{i} (y) ∣ \leq L ∣ x - y ∣$ for all $x, y \in R$ , with a common $L \geq 0$ . Then

$\frac{1}{m} E_{σ} \sup_{f \in F} \sum_{i = 1}^{m} σ_{i} Φ_{i} (f (z_{i})) \leq L {\hat{R}}_{S} (F) .$

Here $S = (z_{1}, \dots, z_{m})$ and ${\hat{R}}_{S} (F) : = m^{- 1} 2^{- m} \sum_{σ \in {- 1, 1}^{m}} \sup_{f \in F} \sum_{i} σ_{i} f (z_{i})$ . Expectations over signs mean this uniform finite average; no measurability on the functions' domain is needed. For measurable classes on a measurable space this agrees with One-sided empirical Rademacher complexity. Equivalently, the unnormalized left expectation is at most $L$ times the unnormalized one-sided supremum on the right.

The same holds for a countable class when both suprema are finite for every sign vector. No condition $Φ_{i} (0) = 0$ is required; additive constants cancel because the proof compares coordinate differences.

Facts & Assumptions

Given: A fixed sample, a nonempty finite class of real-valued functions, and coordinate maps $Φ_{i}$ with common Lipschitz constant $L \geq 0$ .

[F1]

The fixed-sample finite-average convention in the statement gives ${\hat{R}}_{S} (F) = m^{- 1} E_{σ} \sup_{f \in F} \sum_{i} σ_{i} f (z_{i})$ , with no absolute value. On measurable classes it is One-sided empirical Rademacher complexity.

Proof

Given: The finite class, fixed sample, and Lipschitz coordinate maps in the statement.

1.1givenalgebra

Fix a coordinate $k$ , arbitrary real offsets $a_{f}$ for $f \in F$ , and $x_{f} : = f (z_{k})$ . Averaging over $σ_{k}$ gives $E_{σ_{k}} \sup_{f} (a_{f} + σ_{k} Φ_{k} (x_{f})) = \frac{1}{2} \sup_{f, g} (a_{f} + a_{g} + Φ_{k} (x_{f}) - Φ_{k} (x_{g}))$ . The Lipschitz bound makes the last summand at most $L ∣ x_{f} - x_{g} ∣$ . Because ordered pairs include both $(f, g)$ and $(g, f)$ , the supremum with $L ∣ x_{f} - x_{g} ∣$ equals the supremum with $L (x_{f} - x_{g})$ : swap the pair whenever $x_{f} < x_{g}$ . Factoring this last supremum gives $\frac{1}{2} \sup_{f} (a_{f} + L x_{f}) + \frac{1}{2} \sup_{g} (a_{g} - L x_{g}) = E_{σ_{k}} \sup_{f} (a_{f} + σ_{k} L x_{f})$ .

2.1F1step 1.1algebra

Apply step 1.1 successively for $k = m, m - 1, \dots, 1$ . At stage $k$ , condition on all other signs and use $a_{f} : = \sum_{i < k} σ_{i} Φ_{i} (f (z_{i})) + \sum_{i > k} σ_{i} L f (z_{i})$ , so the offsets include both unreplaced and replaced coordinates. Averaging the inequality over the other signs shows that replacing coordinate $k$ cannot decrease the expected supremum. Thus $E_{σ} \sup_{f} \sum_{i} σ_{i} Φ_{i} (f (z_{i})) \leq L E_{σ} \sup_{f} \sum_{i} σ_{i} f (z_{i})$ . Dividing by $m$ and using [F1] gives the statement.

3.1step 2.1given∎

For a countable class, enumerate its members and apply the finite result to each increasing finite initial subclass. For each of the finitely many sign vectors, the suprema increase to the stated finite supremum; taking the finite average over sign vectors passes the inequalities to the limit.

Remarks

Adding constants $c_{i}$ to the coordinate maps adds the same sign sum $\sum_{i} σ_{i} c_{i}$ to every candidate in the supremum. Its sign expectation is zero, so the expected supremum is unchanged; this is why the one-sided result needs no zero-at-zero assumption.

Depends on

One-sided empirical Rademacher complexity

Used by

Correct-scale slab bound for multivariate trimming Proposition
Absolute-value Rademacher contraction Theorem

Dependency tree · two levels

2 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

Mehryar Mohri, Afshin Rostamizadeh, and Ameet Talwalkar, Foundations of Machine Learning, 2nd ed., Lemma 5.7 (standard reference, not scraped)
David Pollard, Empirical Processes: Theory and Applications, Chapter 5 (standard reference, not scraped)