mathlib3

f302c979 - feat(measure_theory/l2_space): the inner product of indicator_const_Lp and a function is the set_integral (#8229)

feat(measure_theory/l2_space): the inner product of indicator_const_Lp and a function is the set_integral (#8229) Co-authored-by: Rémy Degenne <remydegenne@gmail.com> Co-authored-by: RemyDegenne <remydegenne@gmail.com>