3.3 A reproducing kernel Hilbert space
The second family of Corollary 1.4 is the map \(x \mapsto k_x\) to the kernel sections of a reproducing kernel Hilbert space. It is square-integrable with values in a separable Hilbert space, and by Lemma 3.2(a) the quadratic form of its Gram operator is \(\langle g, J g \rangle = \int _\Omega |g|^2 \, d\mu \).
Let \(H\) be a complex Hilbert space of functions on a set \(\Omega \) on which every point evaluation \(f \mapsto f(x)\) is continuous.
(a) For every \(x \in \Omega \) there is \(k_x \in H\) with \(\langle k_x, f \rangle = f(x)\) for every \(f \in H\). With \(K(x, y) = \langle k_y, k_x \rangle \) one has \(K(x, y) = k_x(y)\), so \(k_x = K(x, \cdot )\) and \(K(x, x) = \| k_x\| ^2\), and \(|\langle f, k_x \rangle | = |f(x)|\) for every \(f \in H\).
(b) Let \((\Omega , \mu )\) be a measure space, let \(H\) be separable, and let every \(f \in H\) be measurable. Then \(x \mapsto k_x\) is strongly measurable, and it is square-integrable if \(\int _\Omega K(x, x) \, d\mu (x) {\lt} \infty \).
(a) Evaluation at \(x\) is a continuous linear functional, so the Riesz representation theorem gives \(k_x\). Then \(K(x, y) = \langle k_y, k_x \rangle = k_x(y)\), \(K(x, x) = \| k_x\| ^2\), and \(\langle f, k_x \rangle = \overline{\langle k_x, f \rangle } = \overline{f(x)}\).
(b) Take a Hilbert basis \((e_j)\) of \(H\), which is countable because \(H\) is separable. Then \(k_x = \sum _j \langle e_j, k_x \rangle \, e_j\) with \(\langle e_j, k_x \rangle = \overline{e_j(x)}\), so \(x \mapsto k_x\) is the pointwise limit of finite sums of measurable maps. Its squared norm is \(K(x, x)\).
In Lean a Hilbert space of functions is a Hilbert space \(H\) together with a linear map \(\varphi : H \to \mathbb {C}^{\Omega }\), \(\varphi (f)(x)\) being the value of \(f\) at \(x\). Injectivity of \(\varphi \) is not required; in Corollary 1.4 it follows from the assumption on vanishing functions.