Commit 2025-05-07 04:11 bc796db8

feat(MeasureTheory): integral is monotone/convex if the integrand is monotone/convex (#24341) This PR shows that the function fun b => ∫ x, f x b ∂μ is monotone/antitone/convex/concave whenever the integrand f x is monotone/antitone/convex/concave ae. This will be needed to show that various functions are operator monotone or convex.