feat(Analysis/InnerProductSpace/Reproducing): Lemmata for reproducing kernels#37533
feat(Analysis/InnerProductSpace/Reproducing): Lemmata for reproducing kernels#37533TJHeeringa wants to merge 3 commits intoleanprover-community:masterfrom
Conversation
github-actions
bot
added
the
new-contributor
Welcome new contributor!Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions. In particular, we kindly remind contributors that we have guidelines regarding the use of AI when making pull requests. We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the If you haven't already done so, please come to https://leanprover.zulipchat.com/, introduce yourself, and mention your new PR. Thank you again for joining our community. |
PR summary 18a09f9093Import changes for modified filesNo significant changes to the import graph Import changes for all files
|
Co-authored-by: Monica Omar <[email protected]>
| ⟪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 |
There was a problem hiding this comment.
| lemma norm_kerFun_sq_eq_norm_kernel {x} : ‖kerFun H x‖ ^ 2 = ‖kernel H x x‖ := by | |
| lemma norm_kerFun_sq_eq_norm_kernel (x) : ‖kerFun H x‖ ^ 2 = ‖kernel H x x‖ := by |
| 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 |
There was a problem hiding this comment.
| lemma norm_kerFun_eq_sqrt_norm_kernel {x} : ‖kerFun H x‖ = √‖kernel H x x‖ := by | |
| lemma norm_kerFun_eq_sqrt_norm_kernel (x) : ‖kerFun H x‖ = √‖kernel H x x‖ := by |
| 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‖ := |
There was a problem hiding this comment.
| lemma norm_kernel_le {x y} : ‖kernel H x y‖ ≤ √‖kernel H x x‖ * √‖kernel H y y‖ := | |
| 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 |
There was a problem hiding this comment.
| lemma norm_kernel_sq_le {x y} : ‖kernel H x y‖ ^ 2 ≤ ‖kernel H x x‖ * ‖kernel H y y‖ := by | |
| lemma norm_kernel_sq_le (x y) : ‖kernel H x y‖ ^ 2 ≤ ‖kernel H x x‖ * ‖kernel H y y‖ := by |
3 participants
These are several lemmata regarding pointwise properties of reproducing kernels.
norm_le_sq_norm_mul_diagandnorm_sq_le_norm_mul_diagfollow from Cauchy-Schwartz onkerFunbut are expressed in terms of the kernel. The names containdiagbecause a kernel is an infinite dimension matrix and thuskernel H x xandkernel H y yare diagonal elements.zero_row_iff_zero_diagandzero_col_iff_zero_diaghave the same proof. One implies the other due to the kernel being Hermitian.AI:
I wrote the proofs myself, and then asked Claude to compact them because they were too long and I could see that they could be shortened. It gave some good suggestions but mostly broke the proofs, so fixed and compacted it myself (taking into account its useful suggestions).