mathlib

483dd86c - chore(probability/kernel/basic): split into three files (#18957)

chore(probability/kernel/basic): split into three files (#18957) Split `probability/kernel/basic` into 3 files: - basic: definitions of a kernel, classes of kernels and some elementary kernels - measurable_integral: measurability of the Lebesgue integral against a kernel. I am about to add a lot more material to this file, about (ae-)strong measurability, the Bochner integral, etc. This planned increase in size is the motivation for this PR. - with_density: the kernel `with_density`. It requires results about measurability of the integral, hence it cannot remain in basic.