mathlib3

3b88f400 - feat(probability/kernel/disintegration): disintegration of finite measures on product spaces (#18834)

feat(probability/kernel/disintegration): disintegration of finite measures on product spaces (#18834) Disintegration of finite measures on `α × Ω`, where `Ω` is a standard Borel space. Co-authored-by: RemyDegenne <remydegenne@gmail.com>