mathlib

9c3d3d9b - feat(measure_theory/integral/average): FIrst moment method for the Lebesgue integral