HSIC zero-iff-independent theorem #
Under a characteristic kernel on the product space, HSIC vanishes exactly when the joint distribution equals the product of its marginals.
theorem
hsicDef_zero_iff_independent
{X : Type u_1}
[MeasurableSpace X]
{Y : Type u_2}
[MeasurableSpace Y]
{H : Type u_3}
[NormedAddCommGroup H]
[InnerProductSpace ℝ H]
[CompleteSpace H]
[RKHS ℝ H (X × Y) ℝ]
(hchar : IsCharacteristic)
(P : MeasureTheory.Measure (X × Y))
:
hsicDef P = 0 ↔ P = (MeasureTheory.Measure.map Prod.fst P).prod (MeasureTheory.Measure.map Prod.snd P)
HSIC characterises independence under a characteristic kernel.
hsicDef P = 0 ↔ P = P_X ⊗ P_Y.