[Merged by Bors] - feat(Analysis/InnerProductSpace/Reproducing): lemmata for reproducing kernels

Mathlib/Analysis/InnerProductSpace/Reproducing.lean

@@ -130,6 +130,27 @@ lemma kernel_inner (x y : X) (v w : V) :
     ⟪kernel H x y v, w⟫_𝕜 = ⟪kerFun H y v, kerFun H x w⟫_𝕜 := by
   simp [← adjoint_inner_left, kernel]
 
+lemma norm_kerFun_sq_eq_norm_kernel (x) : ‖kerFun H x‖ ^ 2 = ‖kernel H x x‖ := by
+  rw [sq, ← ContinuousLinearMap.norm_adjoint_comp_self, kernel_apply]
+
+lemma norm_kerFun_eq_sqrt_norm_kernel (x) : ‖kerFun H x‖ = √‖kernel H x x‖ := by
+  rw [← norm_kerFun_sq_eq_norm_kernel, Real.sqrt_sq (norm_nonneg _)]
+
+lemma norm_kernel_le (x y) : ‖kernel H x y‖ ≤ √‖kernel H x x‖ * √‖kernel H y y‖ :=
+  (opNorm_comp_le _ _).trans_eq <| by simp_rw [LinearIsometryEquiv.norm_map,
+    norm_kerFun_eq_sqrt_norm_kernel]
+
+lemma norm_kernel_sq_le (x y) : ‖kernel H x y‖ ^ 2 ≤ ‖kernel H x x‖ * ‖kernel H y y‖ := by
+  rw [← Real.le_sqrt (norm_nonneg _) (mul_nonneg (norm_nonneg _) (norm_nonneg _)),
+    Real.sqrt_mul (norm_nonneg _)]
+  exact norm_kernel_le _ _
+
+theorem norm_kernel_eq_zero_iff (x) : ‖kernel H x x‖ = 0 ↔ ∀ y, ‖kernel H x y‖ = 0 :=
+  ⟨fun h y ↦ (sq_nonpos_iff _).mp <| (norm_kernel_sq_le _ _).trans (by simp [h]), fun h ↦ h x⟩
+
+theorem norm_kernel_eq_zero_iff' (x) : ‖kernel H x x‖ = 0 ↔ ∀ y, ‖kernel H y x‖ = 0 :=
+  ⟨fun h y ↦ (sq_nonpos_iff _).mp <| (norm_kernel_sq_le _ _).trans (by simp [h]), fun h ↦ h x⟩
+
 /-- The span of the kernel functions is dense. -/
 theorem kerFun_dense : topologicalClosure (span 𝕜 {kerFun H x v | (x) (v)}) = ⊤ := by
   refine (orthogonal_eq_bot_iff.mp ((Submodule.eq_bot_iff _).mpr fun f fin ↦ DFunLike.ext f 0 ?_))