mathlib

9b245e23 - feat(analysis/convex/integral): drop an assumption, add a version (#13920)

feat(analysis/convex/integral): drop an assumption, add a version (#13920) * add `convex.set_average_mem_closure`; * drop `is_closed s` assumption in `convex.average_mem_interior_of_set`; * add `ae_eq_const_or_norm_average_lt_of_norm_le_const`, a version of `ae_eq_const_or_norm_integral_lt_of_norm_le_const` for average.