Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge 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.

One-sided Rademacher symmetrization bound

Statement

Let (Z,A,P) be a probability space, let m≥1, and let G be a nonempty class of measurable functions g:Z→[0,1]. Let S=(Z1,…,Zm) be IID with law P, let S′=(Z1′,…,Zm′) be an independent IID copy on a finite product probability extension, and let σ1,…,σm be independent uniform signs independent of both samples. Write Pmg=m−1∑ig(Zi) and Pm′g=m−1∑ig(Zi′). Assume the random suprema sup⁡g(Pg−Pmg), sup⁡g(Pm′g−Pmg), sup⁡g∑iσi(g(Zi′)−g(Zi)), and sup⁡g∑iσig(Zi) are measurable on their respective product sigma algebras. Then, with Rm(G) the expected one-sided Rademacher complexity,

ESsup⁡g∈G(Pg−Pmg)≤2Rm(G).

This is a one-sided expectation inequality; it does not assert a tail bound or an absolute-value deviation bound. No choice axiom is assumed.

Statement references

One-sided Rademacher complexity: Rm(G) is the expected empirical one-sided sign supremum with normalization 1/m.

Mohri et al., Theorem 3.3 proof, printed pp. 31–33: the complete ghost-sample and sign-symmetrization argument for the one-sided bound.

Bartlett and Mendelson, Theorem 8 proof, printed pp. 466–467: an independent ghost-sample proof in their different 2/m absolute-value convention.

Facts & Assumptions

Given: A probability law P, a nonempty measurable [0,1]-valued class, an IID sample, an independent copy, independent uniform signs and the stated measurability of the suprema.

[A1]

The random suprema over the sample, independent copy and signs named in the Statement are measurable.

[F1]

For each g∈G, Pg=∫g dP, Pmg=m−1∑ig(Zi), and Rm(G)=ESEσsup⁡g∈Gm−1∑iσig(Zi). One-sided Rademacher complexity

[F2]

IID means mutual independence with common law; a finite family of independent random elements has product joint law. Identical distribution and IID families, Independent random elements have product joint law

[F3]

For a measurable bounded g and a random element with law P, its expectation is ∫g dP. Change of variables for expectation

[F4]

A finite product measure is determined by its rectangle values. Consequently, permuting coordinates of a finite product of the same probability law preserves that product law. For sigma-finite factors, the product measure exists, has the rectangle formula, is sigma-finite, and is unique

[F5]

Fubini gives equality of product and iterated integrals for an integrable product-measurable function on sigma-finite factors. Here each factor carries a probability measure and is sigma-finite, while the product-measurable sample-copy supremum is bounded on a probability product and hence integrable. Fubini's theorem for L^1 functions on a sigma-finite product

Proof

Given: The objects and hypotheses in the Statement.

1.1A1F1F2F3F5givenalgebra

For each fixed sample S and each g∈G, [F2]–[F3] give ES′Pm′g=Pg, so Pg−Pmg=ES′(Pm′g−Pmg). For any bounded family Xg, sup⁡gEXg≤Esup⁡gXg, since each EXg is at most Esup⁡hXh. Applying this conditionally on S and integrating, with [F5] to identify the iterated and joint product expectations, gives ESsup⁡g(Pg−Pmg)≤ES,S′sup⁡g(Pm′g−Pmg).

2.1A1F2F4step 1.1

By [F2], the 2m coordinates of (S,S′) have product law P2m. For each fixed sign vector, swap Zi and Zi′ exactly when σi=−1. This coordinate permutation preserves the product law by [F4] and sends each difference g(Zi′)−g(Zi) to σi(g(Zi′)−g(Zi)). Averaging over the finite sign space gives ES,S′sup⁡g(Pm′g−Pmg)=ES,S′,σsup⁡gm−1∑iσi(g(Zi′)−g(Zi)).

3.1F1F2step 1.1step 2.1algebra∎

For every pair of samples and sign vector, subadditivity gives sup⁡gm−1∑iσi(g(Zi′)−g(Zi))≤sup⁡gm−1∑iσig(Zi′)+sup⁡gm−1∑i(−σi)g(Zi). The first term has expectation Rm(G) by [F1] and the law of S′; the second has the same expectation because −σ is uniform on the sign cube and S has law Pm by [F2]. Combining with steps 1.1–2.1 proves the result.

Depends on

Used by

Dependency tree · two levels

33 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