6.2 Kernel mean embedding

Definition 6.6 Kernel mean embedding

Lean: kernelMeanEmbedding

For a measure \(P\) on \(X\), set

\[ \mu _P \; :=\; \int _X k_x \, \mathrm{d}P(x) \; \in \; \mathcal{H} \]

(Bochner integral) [ 19 ] .

Theorem 6.7 Reproducing property for the embedding

Lean: kernelMeanEmbedding_reproducing

For integrable \(f\), \(\langle \mu _P, f \rangle \; =\; \int _X f(x) \, \mathrm{d}P(x)\) [ 19 , eq. (4) ] , [ 11 , § 2, eq. (2) ] .

Theorem 6.8 Norm bound

Lean: kernelMeanEmbedding_norm_le

Under IsProbabilityMeasure \(P\), \(\| \mu _P\| \le C\) [ 11 , Lemma 4 ] .

Theorem 6.9 Integrability of the KME integrand

Lean: kernelMeanEmbedding_integrable

Under IsFiniteMeasure \(P\), continuity of \(x \mapsto k_x\), and a bounded kernel, the feature map \(x \mapsto k_x\) is Bochner-integrable against \(P\), so \(\int _X k_x \, \mathrm{d}P(x)\) is well-defined [ 11 , § 2 ] .