Theorem ContDiffBump.integral_le_measure_closedBall

chore: replace `(mu s).toReal` with `mu.real s`, when `mu` is a measure, throughout the library (#24204) …

feat: The convolution of a locally integrable function f with a sequence of bump functions converges ae to f (#6102)