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

Finite-sample representer theorem when a minimizer exists

Statement

Let H be a real reproducing kernel Hilbert space with kernel k, let n≥0, let x1,…,xn be sample points, let L:Rn→R be finite-valued, and let Ω:[0,∞)→R be nondecreasing. Define J(f):=L(f(x1),…,f(xn))+Ω(∥f∥H). If J has a minimizer, then it has a minimizer in span⁡{k(⋅,xi):1≤i≤n}; equivalently, at least one minimizer has the finite expansion f(⋅)=∑i=1nαik(⋅,xi). This is an existence-conditional statement and asserts no minimizer exists when none is separately guaranteed.

Facts & Assumptions

Given: A real RKHS H with kernel k, finitely many sample points, a finite-valued loss L, a nondecreasing penalty Ω, and a minimizer f of J.

[F1]

For each x, the section kx=k(⋅,x) lies in the RKHS and ⟨h,kx⟩=h(x) (Positive semidefinite kernels and reproducing kernel Hilbert spaces).

[F2]

Every finite-dimensional subspace of a real inner-product space admits a unique orthogonal projection, the residual is orthogonal to the subspace, and the projection does not increase norm (Projection onto a finite-dimensional subspace of an arbitrary real inner-product space).

Proof

1.1givenF2construct

Let M:=span⁡{kxi:1≤i≤n}. It is finite-dimensional. Apply [F2] to f and M, and write f=p+h with p∈M and h⊥M.

2.1step 1.1F1algebra

For every i, [F1] gives h(xi)=⟨h,kxi⟩=0, so p(xi)=f(xi). Hence the loss terms in J(p) and J(f) agree.

3.1step 1.1step 2.1F2

The norm-contraction clause of [F2] gives ∥p∥H≤∥f∥H. Monotonicity of Ω therefore gives J(p)≤J(f).

4.1givenstep 3.1∎

Since f is a minimizer, J(f)≤J(p). Thus J(p)=J(f) and p is also a minimizer; by its definition p is a finite linear combination of the sample kernel sections.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

9 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