Reproducing property of the kernel mean embedding #
⟪μ_P, f⟫ = ∫ f dP for every f ∈ H: the inner product of a function
with the kernel mean embedding of P equals the expectation of the
function under P. The proof routes through Mathlib's integral_inner
and the RKHS reproducing property inner_kerFun.
theorem
kernelMeanEmbedding_reproducing
{X : Type u_1}
[TopologicalSpace X]
[MeasurableSpace X]
[OpensMeasurableSpace X]
{H : Type u_2}
[NormedAddCommGroup H]
[InnerProductSpace ℝ H]
[CompleteSpace H]
[SecondCountableTopology H]
[RKHS ℝ H X ℝ]
[BoundedKernel H]
(P : MeasureTheory.Measure X)
[MeasureTheory.IsFiniteMeasure P]
(hcont : Continuous fun (x : X) => (RKHS.kerFun H x) 1)
(f : H)
:
Reproducing property of the kernel mean embedding.
⟪μ_P, f⟫ = ∫ f dP for f ∈ H and P finite.
theorem
rkhs_eval_eq_inner
{X : Type u_1}
{H : Type u_2}
[NormedAddCommGroup H]
[InnerProductSpace ℝ H]
[CompleteSpace H]
[RKHS ℝ H X ℝ]
(f : H)
(x : X)
:
Pointwise reproducing identity: f x = ⟪kerFun H x 1, f⟫.