mathlib

a9545e8a - feat(probability/kernel/basic): integrals of basic kernels (#18961)

feat(probability/kernel/basic): integrals of basic kernels (#18961) Lebesgue and Bochner integral of a function against deterministic, constant and restricted kernels.