Commit 2026-09-01 23:21 0b5e0bcf

View on Github →

feat(Analysis/InnerProductSpace/Reproducing): add outerKernel (#42682) This PR adds the kernel generated from a function f : X → V with the rank-one operators ⟪f x, •⟫ f y as its entries.

Estimated changes

modified theorem Finsupp.mul_sum
modified theorem Finsupp.sum_mul
added theorem RKHS.inner_outerKernel
added def RKHS.outerKernel
added theorem RKHS.outerKernel_apply
added theorem RKHS.outerKernel_inner
added theorem RKHS.outerKernel_zero