ExampleConstruction: AI-generatedVerification: AI-generatedPipeline-generated

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.

Bounded linear predictors have a radius-dependent bound

Example

Let $⟨ u, v ⟩ : = \sum_{j = 1}^{d} u_{j} v_{j}$ and $∥ u ∥_{2} : = \sqrt{\sum_{j = 1}^{d} u_{j}^{2}}$ on $R^{d}$ . Put $X_{R} : = {x \in R^{d} : ∥ x ∥_{2} \leq R}$ with its Borel sigma-algebra, let $m, d \geq 1$ , and let a fixed sample $x_{1}, \dots, x_{m} \in X_{R}$ . Let $B, R \geq 0$ satisfy $B R \leq 1$ . For the loss class

$G : = {g_{w} : X_{R} \to [0, 1], g_{w} (x) = \frac{1 + ⟨ w, x ⟩}{2}, ∥ w ∥_{2} \leq B},$

every $g_{w}$ takes values in $[0, 1]$ on the sample domain ${x : ∥ x ∥_{2} \leq R}$ , and

${\hat{R}}_{S} (G) \leq \frac{B R}{2 \sqrt{m}} .$

Example references

One-sided Rademacher complexity: fixes the empirical one-sided sign-average convention.

Cauchy–Schwarz: $∣ ⟨ u, v ⟩ ∣ \leq ∥ u ∥ ∥ v ∥$ , with equality exactly for linearly dependent vectors: gives the Euclidean inner-product bound used to maximize over the ball.

Cauchy-Schwarz for finite random variables: $E [X Y]^{2} \leq E [X^{2}] E [Y^{2}]$ : bounds the sign-average norm by its second moment.

Facts & Assumptions

Given: The fixed sample, radii $B, R \geq 0$ with $B R \leq 1$ , and independent uniform signs.

[F1]

In a real inner product space, $∣ ⟨ u, v ⟩ ∣ \leq ∥ u ∥ ∥ v ∥$ . Cauchy–Schwarz: $∣ ⟨ u, v ⟩ ∣ \leq ∥ u ∥ ∥ v ∥$ , with equality exactly for linearly dependent vectors

[F2]

For finite random variables, $(E [X Y])^{2} \leq E [X^{2}] E [Y^{2}]$ . Cauchy-Schwarz for finite random variables: $E [X Y]^{2} \leq E [X^{2}] E [Y^{2}]$

[F3]

The empirical complexity is $E_{σ} \sup_{g \in G} m^{- 1} \sum_{i} σ_{i} g (x_{i})$ . One-sided Rademacher complexity

Verification

Given: The objects and hypotheses in the Example.

1.1F1given

For every $w$ in the radius- $B$ ball and every sample point, [F1] gives $∣ ⟨ w, x_{i} ⟩ ∣ \leq B R \leq 1$ . Thus $g_{w} (x_{i}) \in [0, 1]$ , as required for the stated loss class.

1.2F1F3givenconstructalgebra

Put $V_{σ} : = \sum_{i} σ_{i} x_{i}$ . By [F3], ${\hat{R}}_{S} (G) = \frac{1}{2 m} E_{σ} [\sum_{i} σ_{i} + \sup_{∥ w ∥_{2} \leq B} ⟨ w, V_{σ} ⟩]$ . The sign sum has expectation zero. By [F1], $⟨ w, V_{σ} ⟩ \leq B ∥ V_{σ} ∥_{2}$ ; equality is attained at $w = B V_{σ} / ∥ V_{σ} ∥_{2}$ when $V_{σ} \neq 0$ , while both sides are zero when $V_{σ} = 0$ . Therefore ${\hat{R}}_{S} (G) = \frac{B}{2 m} E_{σ} ∥ V_{σ} ∥_{2}$ .

2.1F2step 1.2givenalgebra∎

Apply [F2] with $X = ∥ V_{σ} ∥_{2}$ and $Y = 1$ to get $(E_{σ} ∥ V_{σ} ∥_{2})^{2} \leq E_{σ} ∥ V_{σ} ∥_{2}^{2}$ . Expanding the square and using $E_{σ} [σ_{i} σ_{j}] = 0$ for $i \neq j$ and $1$ for $i = j$ gives $E_{σ} ∥ V_{σ} ∥_{2}^{2} = \sum_{i} ∥ x_{i} ∥_{2}^{2} \leq m R^{2}$ . Substitution in step 1.2 proves ${\hat{R}}_{S} (G) \leq B R / (2 \sqrt{m})$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

16 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.