Integrability of kernel sections under finite measures #
Bounded kernel sections have a uniform norm bound via BoundedKernel, and
finite measures bound the integral of constants. Together these give
Integrable (fun x => kerFun H x 1) P for any finite measure P.
theorem
kernelMeanEmbedding_integrable
{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)
:
MeasureTheory.Integrable (fun (x : X) => (RKHS.kerFun H x) 1) P
Bounded kernel sections are integrable under any finite measure.