mathlib

5da37314 - feat(measure_theory/integral): add formulas for average over an interval (#14132)