mathlib

31a8a276 - feat(probability/kernel/basic): add kernel.with_density (#18463)

feat(probability/kernel/basic): add kernel.with_density (#18463) Kernel with image `(κ a).with_density (f a)` if `function.uncurry f` is measurable, and with image 0 otherwise. If `function.uncurry f` is measurable, it satisfies `∫⁻ b, g b ∂(with_density κ f hf a) = ∫⁻ b, f a b * g b ∂(κ a)`. Co-authored-by: Rémy Degenne <remydegenne@gmail.com>