Commit 2022-05-05 00:25 9b245e23

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.