mathlib3

c14c8fcd - feat(measure_theory/integral/average): Lebesgue average (#19199)

feat(measure_theory/integral/average): Lebesgue average (#19199) Define the Lebesgue integral version of the average of a measurable function and prove the corresponding first moment method.