Commit 2025-12-01 09:24 1cd42ec5

feat: drop a measurability assumption (#32280) If P.map f is a probability measure, then so is P. There is no need to assume that f is aemeasurable because if it's not then P.map f is 0 so it can't be a probability measure.