mathlib3

b40ce7d0 - feat(measure_theory/integral/average): average of constant functions (#16776)

feat(measure_theory/integral/average): average of constant functions (#16776) Also make the API more coherent, by renaming `average_def'` to `average_eq` to match `set_average_eq`. And rename `lintegral_to_real_le_lintegral_nnnorm` to `lintegral_of_real_le_lintegral_nnnorm`.