TheoremStatement: Literature-sourcedProof: AI-generatedPipeline-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.

The kernel ridge system uniquely minimizes the mean-square RKHS objective

Statement

Let $X$ be a set, let $k : X \times X \to R$ be a real positive-semidefinite kernel, and let $H$ be a real reproducing-kernel Hilbert space with kernel $k$ . Take a finite ordered list $X = (x_{i})_{i = 1}^{n}$ with $n \geq 1$ , a response vector $y \in R^{n}$ , and $λ > 0$ . Put $K = (k (x_{i}, x_{j}))_{i, j = 1}^{n}$ and $τ = n λ$ . Define $a = (K + τ I_{n})^{- 1} y$ , $f_{0} = \sum_{i = 1}^{n} a_{i} k (\cdot, x_{i})$ , and $u = K a$ . Then $f_{0}$ is the unique minimizer over $f \in H$ of

$J (f) = \frac{1}{n} \sum_{i = 1}^{n} (y_{i} - f (x_{i}))^{2} + λ ∥ f ∥_{H}^{2},$

and its training evaluation vector is $u = y - τ a$ .

Statement references

Positive semidefinite kernels and reproducing kernel Hilbert spaces: A real RKHS contains each kernel section and satisfies $⟨ f, k (\cdot, x) ⟩_{H} = f (x)$ .

Regularized kernel prediction system: The coefficient and fitted vectors are defined by $a = (K + τ I)^{- 1} y$ and $u = K a = y - τ a$ .

Facts & Assumptions

Given: The kernel, RKHS, training list, response vector, and regularization parameter in the Statement.

[F1]

Positive semidefinite kernels and reproducing kernel Hilbert spaces: each section $k (\cdot, x_{i})$ belongs to $H$ and $⟨ f, k (\cdot, x_{i}) ⟩_{H} = f (x_{i})$ ; every finite Gram matrix of $k$ is symmetric positive semidefinite.

[F2]

Regularized kernel prediction system: $τ = n λ$ , the objective is the mean-square loss plus $λ ∥ f ∥_{H}^{2}$ , and $a = (K + τ I_{n})^{- 1} y$ .

[F3]

Inverse norm bound for a regularized Gram matrix: for $K ⪰ 0$ and $τ > 0$ , $K + τ I_{n}$ is invertible.

Proof

1.1givenF1F2F3constructalgebra

By [F1], $K$ is a real symmetric positive-semidefinite matrix. Let $a = (K + τ I_{n})^{- 1} y$ , which exists by [F2]–[F3], and set $f_{0} = \sum_{i} a_{i} k (\cdot, x_{i})$ . The reproducing identities give $f_{0} (x_{j}) = \sum_{i} a_{i} k (x_{j}, x_{i}) = (K a)_{j}$ , so if $r = y - (f_{0} (x_{i}))_{i = 1}^{n}$ , then $r = y - K a = τ a$ by $(K + τ I_{n}) a = y$ .

2.1givenstep 1.1F1F2algebra

Fix any $h \in H$ . The reproducing identities yield $⟨ f_{0}, h ⟩_{H} = \sum_{i} a_{i} h (x_{i}) = a^{T} (h (x_{i}))_{i = 1}^{n}$ . Expanding both squared norms in $J (f_{0} + h) - J (f_{0})$ gives $\frac{1}{n} ∥ (h (x_{i}))_{i = 1}^{n} ∥_{2}^{2} - \frac{2}{n} r^{T} (h (x_{i}))_{i = 1}^{n} + 2 λ a^{T} (h (x_{i}))_{i = 1}^{n} + λ ∥ h ∥_{H}^{2}$ . Substituting $r = τ a = n λ a$ cancels the two cross terms, leaving $\frac{1}{n} ∥ (h (x_{i})) ∥_{2}^{2} + λ ∥ h ∥_{H}^{2} \geq 0$ .

3.1givenstep 1.1step 2.1algebra∎

Step 2.1 shows $J (f_{0} + h) \geq J (f_{0})$ for every $h$ , so $f_{0}$ is a minimizer. Equality forces $λ ∥ h ∥_{H}^{2} = 0$ , hence $h = 0$ because $λ > 0$ ; the minimizer is unique. The evaluation computation in step 1.1 gives its fitted vector $u = K a = y - τ a$ .

Depends on

Used by

Dependency tree · two levels

8 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

Carl Edward Rasmussen and Christopher K. I. Williams, Gaussian Processes for Machine Learning, Chapter 6 §6.2.2 (standard reference, not scraped)
Per-Gunnar Martinsson and Joel A. Tropp, Randomized Numerical Linear Algebra: Foundations & Algorithms, §19.1.6 (standard reference, not scraped)