Norm bounds for RKHS functions and the kernel mean embedding

Point-evaluation bound: ‖f x‖ ≤ C · ‖f‖ where C = BoundedKernel.bound. RKHS functions are continuous and integrable under finite measures. The kernel mean embedding of a probability measure has norm at most C.

theorem norm_apply_le_bound_mul_norm {X : Type u_1} {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] [RKHS ℝ H X ℝ] [BoundedKernel H] (f : H) (x : X) : ‖f x‖ ≤ BoundedKernel.bound H X * ‖f‖

Pointwise bound on RKHS function evaluations via Cauchy-Schwarz.

theorem continuous_rkhs_apply {X : Type u_1} [TopologicalSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] [RKHS ℝ H X ℝ] (hcont : Continuous fun (x : X) => (RKHS.kerFun H x) 1) (f : H) : Continuous fun (x : X) => f x

x ↦ f x is continuous whenever the kernel section map is.

theorem rkhs_fun_integrable {X : Type u_1} [TopologicalSpace X] [MeasurableSpace X] [OpensMeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace 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) : MeasureTheory.Integrable (fun (x : X) => f x) P

RKHS functions are integrable under any finite measure when the kernel is bounded.

theorem kernelMeanEmbedding_norm_le {X : Type u_1} [MeasurableSpace X] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℝ H] [CompleteSpace H] [RKHS ℝ H X ℝ] [BoundedKernel H] (P : MeasureTheory.Measure X) [MeasureTheory.IsProbabilityMeasure P] : ‖kernelMeanEmbedding P‖ ≤ BoundedKernel.bound H X

Norm of the kernel mean embedding of a probability measure is bounded by the kernel bound.