6.1 Bounded kernels
Lean: BoundedKernel
A BoundedKernel \(\mathcal{H}\) is a witness \(\langle C, h_{\ge 0}, h_{\le } \rangle \) with \(C \ge 0\) and \(\| k_x \| \le C\) for all \(x : X\). Bounded-feature kernels are the canonical setting for kernel mean embeddings [ 21 , § 4.2 ] .
Lean: norm_apply_le_bound_mul_norm
\(|f(x)| \le C \cdot \| f\| \) for every \(f \in \mathcal{H}\) and \(x \in X\) [ 21 , Thm 4.23 ] .
Lean: rkhs_eval_eq_inner
\(f(x) = \langle k_x,\, f \rangle \) for every \(f \in \mathcal{H}\) and \(x \in X\) [ 1 ] .
Lean: continuous_rkhs_apply
If the feature map \(x \mapsto k_x\) is continuous, then every \(f \in \mathcal{H}\) is continuous on \(X\) [ 21 , Lemma 4.29 ] .
Lean: rkhs_fun_integrable
Under IsFiniteMeasure \(P\) and a continuous feature map, every \(f \in \mathcal{H}\) is \(P\)-integrable (via \(L^\infty \subset L^1\) on finite measures).