mathlib

ccdbfb6e - feat(measure_theory/integral/set_integral): First moment method (#18731)

feat(measure_theory/integral/set_integral): First moment method (#18731) Integrable functions are smaller/larger than their mean on a set of positive measure. We prove it for the Bochner and Lebesgue integrals.