Symmetrization Inequality

Let $\mathcal{F}$ be a class of functions $f: \mathcal{Z} \to [0, 1]$ and let $S = (z_1, \ldots, z_n)$ be drawn i.i.d. from $\mathcal{D}$. Then:

$\mathbb{E}_S\!\left[\sup_{f \in \mathcal{F}} (Pf - P_n f)\right] \leq 2\,\mathfrak{R}_n(\mathcal{F})$

where $\mathfrak{R}_n(\mathcal{F}) = \mathbb{E}_{S, \sigma}\!\left[\sup_{f \in \mathcal{F}} \frac{1}{n}\sum_{i=1}^n \sigma_i f(z_i)\right]$ is the Rademacher complexity.

The population expectation $Pf$ is an average over infinitely many points. The empirical expectation $P_n f$ is an average over $n$ points. The gap between them measures how much the finite sample misrepresents the truth.

Symmetrization bounds this gap by measuring how well $\mathcal{F}$ can correlate with random noise (Rademacher complexity). The logic: if the class cannot even fit random labels well, it certainly cannot overfit to the specific noise in the training data.

The factor of 2 is structural, not a proof artifact. It arises from two steps: (1) replacing $Pf$ with $P'_n f$ introduces one factor (bounding the difference of two empirical averages), and (2) dropping the ghost sample to get pure Rademacher averages introduces at most another factor (by the triangle inequality and symmetry of $\sigma_i$).

This theorem is the bridge between the generalization gap (which involves the unknown distribution $\mathcal{D}$) and Rademacher complexity (which can be estimated from data). Every Rademacher-based generalization bound starts here:

1. Apply symmetrization to bound the expected gap by $2\mathfrak{R}_n(\mathcal{F})$
2. Apply McDiarmid's inequality to convert the expected bound into a high-probability bound
3. Bound $\mathfrak{R}_n(\mathcal{F})$ using structural properties of $\mathcal{F}$ (e.g., linear classifiers, kernel classes, neural networks)

Within the uniform-convergence framework, symmetrization is the standard device for connecting empirical performance on training data to the unknown population performance. Stability- and PAC-Bayes-based bounds connect the two via different mechanisms (stability of the learner, KL divergence to a prior).

The bound requires $\mathcal{F}$ to map into a bounded range (here $[0,1]$). For unbounded function classes, the ghost sample trick still works but the Rademacher complexity may not be finite. Also, the factor of 2 can be loose: for one-sided deviations, localized Rademacher complexity techniques can sometimes achieve a tighter constant.

Under mild conditions (see Ledoux and Talagrand 1991, Ch 6), the Rademacher complexity is bounded from above by the centered uniform deviation:

$\mathfrak{R}_n(\mathcal{F}) \leq 2\,\mathbb{E}_S\!\left[\sup_{f \in \mathcal{F}} |P_n f - Pf|\right]$

Together with the symmetrization upper bound, this shows that the expected uniform deviation and the Rademacher complexity are equivalent up to a universal constant. Rademacher complexity is a tight measure of uniform convergence, not merely an upper bound.

Symmetrization is not a lossy reduction. The Rademacher complexity is equivalent to the expected uniform deviation up to a universal constant. This means Rademacher complexity exactly characterizes the rate of uniform convergence, not just an upper bound on it.

This lower bound shows that Rademacher complexity is the right complexity measure for uniform convergence. It is both necessary and sufficient up to a universal constant: the generalization gap scales as $\Theta(\mathfrak{R}_n(\mathcal{F}))$, not just $O(\mathfrak{R}_n(\mathcal{F}))$.

The precise constant depends on whether the class is centered (contains a function with $Pf = 0$, or is translated to that form). For uncentered classes, an extra term involving $\sup_f |Pf|$ can appear. The upper bound (symmetrization) is the direction used in almost all generalization arguments. the lower bound matters mainly when one wants to show that a class is not learnable at a given rate.

Let $\mu$ be a probability measure on a measurable space $\alpha$, let $\iota$ be a finite nonempty index set, and let $g : \iota \to \alpha \to \mathbb{R}$ be such that the suprema $\sup_i g_i$, $\sup_i (-g_i)$, and (for each $z$) $\sup_i (g_i(\cdot) - g_i(z))$ are $\mu$-integrable, with the outer ghost-sample integrand also integrable. Let $\nu$ denote the Rademacher measure on $\mathbb{R}$, $\nu = \tfrac12 \delta_{-1} + \tfrac12 \delta_{1}$. Then:

$\int_\alpha \int_\alpha \sup_{i \in \iota} \big(g_i(z') - g_i(z)\big)\, d\mu(z')\, d\mu(z) \;\le\; 2 \int_\alpha \int_{\mathbb{R}} \sup_{i \in \iota} \big(\sigma\, g_i(z)\big)\, d\nu(\sigma)\, d\mu(z).$

This is the finite-class, single-shared-Rademacher-sign form of the symmetrization estimate. It is the statement closed in TheoremPath.Statistics.Rademacher.oneSampleFiniteClassSymmetrization (see the Lean manifest entry claim:symmetrization-inequality::one-sample-finite-class-symmetrization).

Lean-verified finite one-sample symmetrization lemma. The full finite-sample iid Rademacher symmetrization theorem (the statement above in Main Theorems, with empirical means $\tfrac{1}{n}\sum_{i=1}^n f(z_i)$ and $n$ independent Rademacher signs $\sigma_1, \ldots, \sigma_n$) remains in progress.

Replacing $z$ with a single $\sigma \in \{-1, +1\}$ and the function family $\{f \in \mathcal{F}\}$ with a finite indexed family $g : \iota \to \alpha \to \mathbb{R}$ removes two pieces of infrastructure: the $n$-fold product measure $\mu^{\otimes n}$ and the joint distribution of $n$ independent Rademacher signs. What remains is the structural core of the argument: the sup-triangle, the two-point expectation expansion, and the fact that the $\sigma$-integral of $\sup_i (\sigma\, g_i(z))$ equals $\tfrac12 \sup_i (-g_i(z)) + \tfrac12 \sup_i g_i(z)$.

This is the smallest scoped form of symmetrization that captures the sup-triangle and the two-point Rademacher expectation in a single proven statement. It is not a substitute for the full $n$-sample iid Rademacher symmetrization theorem above, which requires building a product Rademacher measure and a Fubini argument over $\mu^{\otimes n}$. The remaining gap to that full theorem is documented in docs/plans/symmetrization-lean-plan.md.

The bound is one-sided in $\sigma$ (a single shared sign, not $n$ independent signs), so the right-hand side here is not the empirical Rademacher complexity $\mathfrak{R}_n(\mathcal{F})$ in the standard $\tfrac{1}{n}\sum_{i=1}^n \sigma_i\, f(z_i)$ form. Do not cite this verified lemma as evidence for the full theorem; the public claim claim:symmetrization-inequality::symmetrization-inequality-theorem remains source-checked but not Lean-verified.

Let $\mu$ be a probability measure on a measurable space $Z$, let $\iota$ be a finite nonempty index set, and let $\ell : \iota \to Z \to \mathbb{R}$ be a family of measurable functions with $|\ell_i(z)| \le B$ for all $i, z$. Let $S = (z_1, \ldots, z_n)$ be drawn iid from $\mu$, and let $\mathfrak{R}_n(\ell, S)$ denote the empirical Rademacher complexity of $\ell$ on $S$ (averaged against the uniform sign vector). Then for $n \ge 1$:

$\mathbb{E}_{S \sim \mu^{\otimes n}}\!\left[\sup_{i \in \iota}\big(R(\ell_i) - \widehat{R}_S(\ell_i)\big)\right] \;\le\; 2\, \mathbb{E}_{S \sim \mu^{\otimes n}}\!\left[\mathfrak{R}_n(\ell, S)\right].$

Here $R(\ell_i) = \int_Z \ell_i\, d\mu$ is the population risk and $\widehat{R}_S(\ell_i) = \tfrac{1}{n}\sum_{k=1}^n \ell_i(z_k)$ is the empirical risk on $S$. The statement is closed in TheoremPath.LearningTheory.RademacherSymmetrization.expected_genGap_le_two_expected_empiricalRademacherComplexity (see the Lean manifest entry claim:symmetrization-inequality::finite-sample-rademacher-symmetrization).

This is the canonical $n$-sample iid form of the symmetrization inequality, in expectation. The $n$ ghost-sample variables and $n$ independent Rademacher signs both live as iid product measures, and the proof goes through Fubini against $\mu^{\otimes n} \otimes \mu^{\otimes n}$ on $Z^n \times Z^n$.

This is the expected-form analog of the textbook symmetrization inequality restricted to a finite, uniformly bounded index family. With this in hand, the next standard step is McDiarmid's bounded-differences inequality to convert expectation into a high-probability bound. Until that step is formalized, no high-probability Rademacher generalization bound is Lean-verified on this site.

The verified statement is restricted to a finite nonempty index set $\iota$ and bounded loss $|\ell_i(z)| \le B$. It is not a result for infinite or VC-class hypothesis families. It is also an expectation-form bound: it does not produce a high-probability inequality $\Pr(\sup_i (R(\ell_i) - \widehat{R}_S(\ell_i)) \ge t) \le \cdots$. The latter requires McDiarmid concentration, which is planned but not yet verified. The page-level claim claim:symmetrization-inequality::symmetrization-inequality-theorem remains source-checked, not Lean-verified, and there is no page-level Lean badge.