ExampleConstruction: AI-adaptedVerification: 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.

A two-function class on a Bernoulli sample

Example

Let $X = {0, 1}$ with $P ({0}) = P ({1}) = 1 / 2$ . Let $Z \sim P$ , and take the two-function class $F = {f_{0}, f_{1}}$ with $f_{0} (x) = 0$ and $f_{1} (x) = x$ .

Facts & Assumptions

Given: The Bernoulli probability space, the observation $Z$ , and the class $F$ .

[F1]

$P f = \int f d P$ , $P_{1} f = f (Z)$ , and the empirical Rademacher process is $σ f (Z)$ (Empirical, centered, and Rademacher processes).

[F2]

For one observation, ${\hat{R}}_{(Z)} (F) = E_{σ} \sup_{f \in F} σ f (Z)$ (One-sided empirical Rademacher complexity).

[F3]

A finite nonempty class of measurable $[0, 1]$ -valued functions satisfies $P (\sup_{f \in F} ∣ P_{n} f - P f ∣ \geq ϵ) \leq 2 ∣ F ∣ e^{- 2 n ϵ^{2}}$ for every $ϵ > 0$ (Uniform deviation bound for a finite unit-range class).

Proof

Given: The sample and class of the Example.

1.1F1givenalgebra

Direct evaluation gives $P f_{0} = 0$ , $P f_{1} = 1 / 2$ , $P_{1} f_{0} = 0$ , and $P_{1} f_{1} = Z$ . Hence $\sup_{f \in F} ∣ P_{1} f - P f ∣ = ∣ Z - 1 / 2 ∣ = 1 / 2$ for both possible observations.

2.1F2step 1.1algebra

If $Z = 0$ , then $\sup_{f} σ f (Z) = 0$ for either sign. If $Z = 1$ , then $\sup_{f} σ f (Z) = \max (0, σ)$ , whose uniform-sign expectation is $1 / 2$ . Thus ${\hat{R}}_{(Z)} (F) = Z / 2$ and its expectation over the sample is $1 / 4$ .

3.1F3step 1.1∎

Applying [F3] with $n = 1$ and $∣ F ∣ = 2$ gives $P (\sup_{f \in F} ∣ P_{1} f - P f ∣ \geq ϵ) \leq 4 e^{- 2 ϵ^{2}}$ for every $ϵ > 0$ . At $ϵ = 1 / 2$ the event has probability one by step 1.1, and the displayed estimate is the stated finite-class guarantee for this class.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

23 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., Chapter 3 (standard reference, not scraped)
Philippe Rigollet and Jan-Christian Hütter, High-Dimensional Statistics: Lecture Notes, Chapter 1 (standard reference, not scraped)