Kernel mean embedding: definition and BoundedKernel class

BoundedKernel is the integrability certificate: its instance carries a uniform bound C on the kernel sections x ↦ kerFun H x 1, which is what lets Bochner integration on a finite measure converge.

kernelMeanEmbedding P := ∫ x, kerFun H x 1 ∂P is the Bochner integral of the kernel sections against P; it lives in the RKHS H.

class BoundedKernel (H : Type u_1) [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] {X : Type u_2} [RKHS ℝ H X ℝ] : Type

An RKHS with a uniform norm bound on its kernel sections. Integrability of the kernel sections under any finite measure reduces to this bound plus AEStronglyMeasurable.

• bound : ℝ
• bound_nonneg : 0 ≤ bound H X
• norm_kerFun_le (x : X) : ‖(RKHS.kerFun H x) 1‖ ≤ bound H X

noncomputable def kernelMeanEmbedding {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] [RKHS ℝ H X ℝ] (P : MeasureTheory.Measure X) : H

The kernel mean embedding of a measure P into the RKHS H, defined as the Bochner integral of the kernel sections.

Equations

• kernelMeanEmbedding P = ∫ (x : X), (RKHS.kerFun H x) 1 ∂P