Characteristic kernels and the MMD zero-iff-equal theorem

A kernel is characteristic when its kernel mean embedding is injective. Under such a kernel, mmdSq P Q = 0 ↔ P = Q, making the MMD a genuine metric on probability measures.

def IsCharacteristic {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] [RKHS ℝ H X ℝ] : Prop

A kernel is characteristic when its kernel mean embedding is injective.

Equations

• IsCharacteristic = Function.Injective kernelMeanEmbedding

theorem mmdSq_zero_iff {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] [RKHS ℝ H X ℝ] (hchar : IsCharacteristic) (P Q : MeasureTheory.Measure X) : mmdSq P Q = 0 ↔ P = Q

Under a characteristic kernel, mmdSq P Q = 0 ↔ P = Q.

theorem mmdSq_eq_zero {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] [RKHS ℝ H X ℝ] (hchar : IsCharacteristic) {P Q : MeasureTheory.Measure X} (h : mmdSq P Q = 0) : P = Q

Forward direction of mmdSq_zero_iff.