§3, Theorem — reproducing kernels of finite-dimensional classes

Proved

AronszajnRK.Sum.finite_dimensional_classes

by mikedeng1 · Oct 4, 2026 · Mathlib 0df444a (Lean v4.33.1)

finite-dimensionalp2o-batch-pfp1bp2o-gran-per-chapterp2o-plan-paperp2o-v1reproducing-kernelsrkhs

Let $E$ be a set. A function $K:E\times E\to\mathbb C$ is the reproducing kernel of a finite-dimensional complex Hilbert space of functions on $E$ if and only if it has the form

K(x,y)=\sum_{i,j=1}^{n}\beta_{ij}\,w_i(x)\,\overline{w_j(y)}\qquad(6)

for some $n\ge 0$ , a positive definite Hermitian matrix $\{\beta_{ij}\}$ and linearly independent functions $w_1,\dots,w_n$ on $E$ . In that case the class $F$ with kernel $K$ is finite-dimensional and generated by the $w_k$ : its functions are exactly

f=\sum_{k=1}^n\zeta_k w_k,\qquad \zeta_k\in\mathbb C,\qquad(1)

and the norm of such an $f$ is

\|f\|^2=\sum_{i,j=1}^n\alpha_{ij}\,\zeta_i\,\bar\zeta_j,\qquad(2)

where $\{\alpha_{ij}\}$ is the inverse of the matrix $\{\bar\beta_{ij}\}$ .

The theorem describes completely the kernels of finite-dimensional spaces: $\{\alpha_{ij}\}=\{(w_i,w_j)\}$ is the Gram matrix of the generating functions.

Formalization Note "Positive definite" is Mathlib's Matrix.PosDef over ℂ (Hermitian with positive quadratic form); $\{\bar\beta_{ij}\}$ is the entrywise conjugate β.map star, not the conjugate transpose. The "only if" direction is stated for every finite-dimensional RKHS; the "if" direction asserts existence of a finite-dimensional RKHS with kernel (6) and describes every RKHS with that kernel. The value $\|f\|^2$ is compared as a complex number with the (real) right-hand side. Checked by hand at $n=1$ : $\alpha=1/\bar\beta=\|w_1\|^2$ .

Preamble

import Mathlib
import Definitions.Def_AronszajnRK_Sum_kernelFn

open scoped ComplexOrder

Formal statement

namespace AronszajnRK.Sum

universe u v

/-- **Reproducing kernels of finite-dimensional classes** (Aronszajn, *Theory of Reproducing
Kernels*, Trans. Amer. Math. Soc. 68 (1950), §3, Theorem, p. 347 (PDF 11), with §3 (1), (2), (6),
p. 346 (PDF 10)). A function `K(x, y)` is the reproducing kernel of a finite-dimensional class of
functions if and only if it is of the form (6) `K(x, y) = ∑ᵢⱼ βᵢⱼ wᵢ(x) \overline{wⱼ(y)}` with a
positive definite matrix `{βᵢⱼ}` and linearly independent functions `wₖ(x)`. The corresponding class
`F` is then generated by the functions `wₖ(x)`, the functions `f ∈ F` given by (1)
`f = ∑ ζₖ wₖ`, and the corresponding norm given by (2) `‖f‖² = ∑ᵢⱼ αᵢⱼ ζᵢ ζ̄ⱼ`, where `{αᵢⱼ}` is
the inverse matrix of `{β̄ᵢⱼ}` (entrywise conjugate, no transpose). -/
theorem finite_dimensional_classes {X : Type u} :
    (∀ (H : Type v) [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
      [RKHS ℂ H X ℂ], FiniteDimensional ℂ H →
        ∃ (n : ℕ) (β : Matrix (Fin n) (Fin n) ℂ) (w : Fin n → X → ℂ),
          β.PosDef ∧ LinearIndependent ℂ w ∧
          kernelFn H = fun x y => ∑ i, ∑ j, β i j * w i x * star (w j y)) ∧
    ∀ (n : ℕ) (β : Matrix (Fin n) (Fin n) ℂ) (w : Fin n → X → ℂ),
      β.PosDef → LinearIndependent ℂ w →
        (∃ (H : Type u) (_ : NormedAddCommGroup H) (_ : InnerProductSpace ℂ H)
            (_ : CompleteSpace H) (_ : RKHS ℂ H X ℂ), FiniteDimensional ℂ H ∧
            kernelFn H = fun x y => ∑ i, ∑ j, β i j * w i x * star (w j y)) ∧
        ∀ (H : Type v) [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
          [RKHS ℂ H X ℂ],
          kernelFn H = (fun x y => ∑ i, ∑ j, β i j * w i x * star (w j y)) →
            FiniteDimensional ℂ H ∧
            Set.range (fun f : H => (f : X → ℂ)) =
              {g : X → ℂ | ∃ ζ : Fin n → ℂ, g = ∑ k, ζ k • w k} ∧
            ∀ (f : H) (ζ : Fin n → ℂ), (f : X → ℂ) = ∑ k, ζ k • w k →
              ((‖f‖ ^ 2 : ℝ) : ℂ) =
                ∑ i, ∑ j, (β.map star)⁻¹ i j * ζ i * star (ζ j) := by sorry

end AronszajnRK.Sum

Source

Aronszajn, Theory of Reproducing Kernels, Trans. Amer. Math. Soc. 68 (1950), p. 347, §3, Theorem; with §3 (1), (2), (6), p. 346

Human review

Endorsed by Shuze Chen · Oct 4, 2026
Confirmed by the moderator at approval.
Endorsed by mikedeng1 · Oct 4, 2026
Confirmed by the mission captain (proposal self-audit).

View graph