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

[TJHeeringa]

---

These are several lemmata regarding pointwise properties of reproducing kernels.

norm_le_sq_norm_mul_diag and norm_sq_le_norm_mul_diag follow from Cauchy-Schwartz on kerFun but are expressed in terms of the kernel. The names contain diag because a kernel is an infinite dimension matrix and thus kernel H x x and kernel H y y are diagonal elements.

zero_row_iff_zero_diag and zero_col_iff_zero_diag have 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).

[github-actions]

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 awaiting-author tag, or another reason described in the Lifecycle of a PR. The review dashboard has a dedicated webpage which shows whether your PR is on the review queue, and (if not), why.

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.

[github-actions]

PR summary 39328e9cd8

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ adjoint_comp_self_eq_zero_iff
+ norm_kerFun_eq_sqrt_norm_kernel
+ norm_kernel_eq_norm_kerFun_sq
+ norm_kernel_le
+ norm_kernel_sq_le

You can run this locally as follows

## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[TJHeeringa]

I updated the implicit {x} to explicit (x) as you suggested. I did this also in the norm_kernel_eq_zero_iff you didn't highlight. I hope that that is correct.

[themathqueen]

I think the first four (or maybe all?) of your results should have H explicit. But I'm not entirely sure. Maybe someone else has an opinion on this.

[TJHeeringa]

I think the first four (or maybe all?) of your results should have H explicit. But I'm not entirely sure. Maybe someone else has an opinion on this.

You mean because the results apply to the kernel of H, and there is not something else that really fixes H for you?
It makes sense in a way to have it explicit because of that. I hadn't done so, because the existing results already in the file have a similar construction but they have H implicit.

[themathqueen]

You mean because the results apply to the kernel of H, and there is not something else that really fixes H for you?

Yup. But let's wait for another opinion on this

[Maldooor]

You mean because the results apply to the kernel of H, and there is not something else that really fixes H for you? It makes sense in a way to have it explicit because of that. I hadn't done so, because the existing results already in the file have a similar construction but they have H implicit.

I think kerFun_apply, kernel_apply, kernel_inner and kerFun_dense not having H be explicit was just an oversight by me so they should probably be me made to have H explicit alongside the lemmas you wrote.

[themathqueen]

Thanks! Looks good. Just two small comments.

maintainer delegate?

[github-actions]

🚀 Pull request has been placed on the maintainer queue by themathqueen.

[j-loreaux]

bors d+

[mathlib-bors]

✌️ TJHeeringa can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[TJHeeringa]

bors r+

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• ci (staging) / Build
• ci (staging) / Post-Build Step
• ci (staging) / Lint style
• ci (staging) / Post-CI job