6.3 Maximum Mean Discrepancy
Definition
6.10
Squared MMD
Lean: mmdSq
\(\mathrm{MMD}^2(P, Q) \; :=\; \| \mu _P - \mu _Q \| ^2\) [ 11 , Defn. 2 ] .
Theorem
6.11
Non-negativity of \(\mathrm{MMD}^2\)
Lean: mmdSq_nonneg
\(\mathrm{MMD}^2(P, Q) \ge 0\) [ 11 , Lemma 5 ] .
Theorem
6.12
\(\mathrm{MMD}^2\) on identical measures
Lean: mmdSq_self
\(\mathrm{MMD}^2(P, P) = 0\) [ 11 , Lemma 5 ] .
Theorem
6.13
Symmetry of \(\mathrm{MMD}^2\)
Lean: mmdSq_comm
\(\mathrm{MMD}^2(P, Q) = \mathrm{MMD}^2(Q, P)\) [ 11 , Lemma 5 ] .
Definition
6.14
Characteristic RKHS
Lean: IsCharacteristic
\(\mathcal{H}\) is characteristic on \(X\) iff the kernel mean embedding \(P \mapsto \mu _P\) is injective. This is the modern definition [ 20 , Defn. 6 ] .
Theorem
6.15
Zero-iff-equal under characteristic kernel
Theorem
6.16
Forward direction: equal measures \(\Rightarrow \) zero MMD
Lean: mmdSq_eq_zero
\(P = Q \Rightarrow \mathrm{MMD}^2(P, Q) = 0\) (direct consequence of \(\mu _P = \mu _Q\)) [ 11 , Lemma 5 ] .